Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000629Frama-CPlug-in > jessiepublic2010-11-16 12:142010-11-17 12:34
ReporterAstra 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000629: Incorrect processing of "type var[]" constructions
DescriptionDuring the processing of axiomatic Permut (taken from the ACSL specification file, page 51) Frama gives the next message: tester@ubuntu-fm:~/workspace/prac1$ frama-c -jessie -jessie-atp gui qsorti.c [kernel] preprocessing with "gcc -C -E -I. -dD qsorti.c" [jessie] Starting Jessie translation qsorti.c:27:[jessie] failure: Unexpected failure. Please submit bug report (Ref. "norm.ml:1533:10"). [kernel] The full backtrace is: Raised at file "src/kernel/log.ml", line 506, characters 30-31 Called from file "src/kernel/log.ml", line 500, characters 2-9 Re-raised at file "src/kernel/log.ml", line 503, characters 8-9 Called from file "src/lib/type.ml", line 746, characters 40-45 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 50, characters 4-20 Called from file "src/kernel/cmdline.ml", line 170, characters 4-8 Plug-in jessie aborted because of an internal error. Please report as 'crash' at http://bts.frama-c.com Specified line number corresponds to the next axiom: @ axiom permut_exchange{L1,L2} : @ \forall double t1[], double t2[], integer i, integer j, integer n; @ \at(t1[i],L1) == \at(t2[j],L2) && @ \at(t1[j],L1) == \at(t2[i],L2) && @ (\forall integer k; 0 <= k < n && k != i && k != j ==> @ \at(t1[k],L1) == \at(t2[k],L2)) @ ==> permut{L1,L2}(t1,t2,n); The same message is displayed while attempting to process the predicate Swap: @ predicate Swap{L1,L2}(int a[], integer i, integer j) = @ \at(a[i],L1) == \at(a[j],L2) && @ \at(a[j],L1) == \at(a[i],L2) && @ \forall integer k; k != i && k != j @ ==> \at(a[k],L1) == \at(a[k],L2); The reason is the incorrect processing of constructions like "type var[]". The equal construction "type* var" causes no error.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001282)
pascal (reporter)
2010-11-16 15:04

You have the correct diagnosis. Indeed, we forgot to run frama-c on the examples in our own documentation. Sorry. This commit in the development version contains the same fixes that you have found by yourself: svn diff -r 7739:7740 Index: flag.c =================================================================== --- flag.c (revision 7739) +++ flag.c (revision 7740) @@ -3,7 +3,7 @@ @ c == BLUE || c == WHITE || c == RED ; @*/ -/*@ predicate permut{L1,L2}(color t1[], color t2[], integer n) = +/*@ predicate permut{L1,L2}(color *t1, color *t2, integer n) = @ \at(\valid_range(t1,0,n),L1) && \at(\valid_range(t2,0,n),L2) && @ \numof(0,n,\lambda integer i; \at(t1[i],L1) == BLUE) == @ \numof(0,n,\lambda integer i; \at(t2[i],L2) == BLUE) @@ -33,7 +33,7 @@ @ \forall integer k; 0 <= k < f.n ==> isColor(f.colors[k]) ; @*/ -/*@ predicate isMonochrome{L}(color t[], integer i, integer j, +/*@ predicate isMonochrome{L}(color *t, integer i, integer j, @ color c) = @ \forall integer k; i <= k <= j ==> t[k] == c ; @*/ Index: permut.c =================================================================== --- permut.c (revision 7739) +++ permut.c (revision 7740) @@ -1,22 +1,22 @@ /*@ axiomatic Permut { - @ // permut{L1,L2}(t1,t2,n) is true whenever t1[0..n-1] in state L1 - @ // is a permutation of t2[0..n-1] in state L2 - @ predicate permut{L1,L2}(double t1[], double t2[], integer n); + @ // permut{L1,L2}(t1,t2,n) is true whenever t1[0..n-1] in state L1 + @ // is a permutation of t2[0..n-1] in state L2 + @ predicate permut{L1,L2}(double *t1, double *t2, integer n); @ axiom permut_refl{L}: - @ \forall double t[], integer n; permut{L,L}(t,t,n); + @ \forall double *t, integer n; permut{L,L}(t,t,n); @ axiom permut_sym{L1,L2} : - @ \forall double t1[], t2[], integer n; + @ \forall double *t1, *t2, integer n; @ permut{L1,L2}(t1,t2,n) ==> permut{L2,L1}(t2,t1,n) ; @ axiom permut_trans{L1,L2,L3} : - @ \forall double t1[], t2[], t3[], integer n; - @ permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n) + @ \forall double *t1, *t2, *t3, integer n; + @ permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n) @ ==> permut{L1,L3}(t1,t3,n) ; @ axiom permut_exchange{L1,L2} : - @ \forall double t1[], t2[], integer i, j, n; + @ \forall double *t1, *t2, integer i, j, n; @ \at(t1[i],L1) == \at(t2[j],L2) && @ \at(t1[j],L1) == \at(t2[i],L2) && @ (\forall integer k; 0 <= k < n && k != i && k != j ==> - @ \at(t1[k],L1) == \at(t2[k],L2)) - @ ==> permut{L1,L2}(t1,t2,n); + @ \at(t1[k],L1) == \at(t2[k],L2)) + @ ==> permut{L1,L2}(t1,t2,n); @ } @*/

- Issue History
Date Modified Username Field Change
2010-11-16 12:14 Astra New Issue
2010-11-16 12:14 Astra Status new => assigned
2010-11-16 12:14 Astra Assigned To => cmarche
2010-11-16 15:04 pascal Note Added: 0001282
2010-11-17 12:34 cmarche Severity crash => minor


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker