Bug #406

etf-reach -c segfaults with ETF output

Added by Anonymous about 10 years ago. Updated almost 10 years ago.

Status:ClosedStart date:03 Aug 2010
Priority:NormalDue date:
Assignee:-% Done:

100%

Category:toolsSpent time:6.00 hours
Target version:ltsmin-1.6

Description

etf-reach -c one-label.etf 1.etf

etf-reach: Exploration order is bfs
etf-reach: ETF language module initialized
etf-reach: opening ../../one-label.etf
etf-reach: The state length is 2
etf-reach: done
etf-reach: There are 1 edge labels
etf-reach: done
etf-reach: initial state found
etf-reach: added map 0 (shape:shape) with 2 entries
etf-reach: added map 1 (multiplicity:multiplicity) with 4 entries
etf-reach: reading values for sort action
etf-reach: read 2 values
etf-reach: reading values for sort multiplicity
etf-reach: read 2 values
etf-reach: parsing finished
etf-reach: success!
etf-reach: creating a new string index
etf-reach: creating a new string index
etf-reach: creating a new string index
etf-reach: parsing table 0
etf-reach: length is 1
etf-reach: table 0 has 2 states and 1 transitions
etf-reach: parsing table 1
etf-reach: length is 1
etf-reach: table 1 has 2 states and 1 transitions
etf-reach: parsing map 0
etf-reach: parsing map 1
etf-reach: Setting values for type 0 (multiplicity)
etf-reach: Setting values for type 1 (shape)
etf-reach: Setting values for type 2 (action)
etf-reach: Creating an AtermDD list domain.
etf-reach: length is 2, there are 2 groups
etf-reach: got initial state
etf-reach: level 0 has 1 states ( 4 nodes )
etf-reach: visited 0 has 1 states ( 4 nodes )
etf-reach: level 1 has 2 states ( 6 nodes )
etf-reach: visited 1 has 3 states ( 7 nodes )
etf-reach: level 2 has 1 states ( 4 nodes )
etf-reach: visited 2 has 4 states ( 6 nodes )
etf-reach: Exploration took 6 group checks and 6 next state calls
etf-reach: reachability took 0.000 real 0.000 user 0.000 sys
state space has 4 states
( 6 final BDD nodes; 7 peak nodes; 6 peak nodes per level )
etf-reach: Symbolic tables have 2 reachable transitions

Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_PROTECTION_FAILURE at address: 0x00007fff5bc00ff8
0x0000000100009b44 in dm_project_vector (m=0x10040e440, row=0, src=0x7fff5bc01090, tgt=0x7fff5bc01010) at dm.c:1193
1193    {
(gdb) 

This is with current maint.

one-label.etf - Test case (389 Bytes) Anonymous, 03 Aug 2010 23:10

Associated revisions

Revision 90d19ee4
Added by Michael Weber about 10 years ago

Fix non-overridden methods for wrappers

(Closes #406)

History

#1 Updated by Anonymous about 10 years ago

  • Assignee changed from Anonymous to Anonymous

The actual problem is that etf-greybox etf_state_short uses an invalid context.

Trace:
in
spec-reach: do_output()
at line
vset_enum(patterns,enum_map,&ctx);
this calls enum_map
spec-reach: enum_map() int val=GBgetStateLabelShort(model, ctx->mapno, src)
this calls etf_state_short(self, label, *state);
which does
GBgetContext(self);

With --cache, the context is replaced with the cache context, and the call
SIlookupC(ctx->label_key_idx[label], (char*)state, len<<2)
segfaults.

#2 Updated by Anonymous about 10 years ago

  • Status changed from New to Assigned
  • % Done changed from 0 to 100

Current maint (90d19ee) contains a proposal how to fix this.

#3 Updated by Anonymous about 10 years ago

  • Status changed from Assigned to Resolved

#4 Updated by Anonymous almost 10 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF