Crah with the option -ulevel

ID0001768: This issue was created automatically from Mantis Issue 1768. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001768	Frama-C	Plug-in > slicing	public	2014-04-30	2015-03-17

Reporter	nguenaomer	Assigned To	patrick	Resolution	fixed
Priority	normal	Severity	crash	Reproducibility	always
Platform	PC	OS	Ubuntu	OS Version	13.04
Product Version	Frama-C Fluorine-20130601	Target Version	-	Fixed in Version	Frama-C Sodium

Description :

When I execute $frama-c fsm.c -main main -slice-pragma main -ulevel 10 -then-on 'Slicing export' -print frama-c get crash with the following part of the log: [slicing] making slicing project 'Slicing'... [slicing] interpreting slicing requests from the command line... [kernel] Current source was: fsm.c:46 The full backtrace is: Raised at file "src/logic/logic_interp.ml", line 796, characters 6-39 Called from file "list.ml", line 75, characters 12-15

Additional Information :

the program produce an output with the option -slevel

Steps To Reproduce :

Here is fsm.c: int choix ; int state = 1; int cumul =0 ; int step =0;

//initialisation

/*@ ensures \result==0 || \result==1 || \result==2 ; */ int choisir() ;

void lecture() { choix = choisir() ; }

void fsm_transition() { switch (state) { case 1: if (choix == 2) { cumul = cumul +2 ; state = 2 ; } else cumul++; break ; case 2: if ((step==50) && (choix==1)) state = 3 ; else cumul++ ; break ; case 3: if ((choix==0) && (cumul==10)) state = 1; default: break ; } }

int main() {

while (step>=0){ lecture() ; fsm_transition() ; if (state == 3) { /@ slice pragma ctrl ;/ break ; } step ++ ; } return 0 ; }