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