2021-01-26 06:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001161Frama-CPlug-in > jessiepublic2012-04-17 22:12
Reporternmuller 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001161: error in wp_behav.c
DescriptionThe following file does not pass the analysis (the resulting trace is supplied in additional informations)

Additional Informationframa-c -jessie -jessie-atp alt-ergo wp_behav1.c
[kernel] preprocessing with "gcc -C -E -I. -dD wp_behav1.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir wp_behav1.jessie
[jessie] File wp_behav1.jessie/wp_behav1.jc written.
[jessie] File wp_behav1.jessie/wp_behav1.cloc written.
[jessie] Calling Jessie tool in subdir wp_behav1.jessie
Generating Why function f
Generating Why function min
Generating Why function bhv
Generating Why function stmt_contract
Generating Why function local_named_behavior
File "jc/jc_interp.ml", line 2965, characters 7-7:
Uncaught exception: File "jc/jc_interp.ml", line 2965, characters 7-13: Assertion failed
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs wp_behav1.cloc wp_behav1.jc
TagsNo tags attached.
Attached Files
  • c file icon wp_behav.c (1,145 bytes) 2012-04-16 12:02 -
    /*@
      @ ensures \result > x;
      @ behavior x1:
      @   assumes x == 1;
      @   ensures \result == 3;
      @ behavior x2:
      @   assumes x == 2;
      @   ensures \result == 4;
      @
    */
    int f (int x) {
      x++;
      //@ for x1: assert x == 2;
      //@ for x2: assert x == 3;
      return x+1;
    }
    
    /*@
        behavior bx :
           assumes x <= y;
           ensures \result == x;
        behavior by :
           assumes x > y;
           ensures \result == y;
        complete behaviors bx, by;
        disjoint behaviors bx, by;
    */
    int min (int x, int y) {
      return (x < y) ? x : y;
    }
    
    /*@ requires n != 0;
      behavior pos :
        assumes n > 0;
        ensures \result == x/n;
      behavior neg :
        assumes n < 0;
        ensures \result == x/-n;
      complete behaviors pos, neg; // notice that this needs the requires hyp
    */
    int bhv (int x, int n) {
      n = (n<0) ? -n : n;
      return x/n;
    }
    
    int stmt_contract (int c) {
      int x = 0;
    
      /*@ requires x == 0;
        @ ensures x > 0;
        */
      if (c)
        x = 3;
      else
        x = 5;
      return x;
    }
    
    int local_named_behavior (int x) {
      int y = 3;
      /*@ behavior xpos :
            assumes x > 0;
            ensures x > 3;
    	*/
      x += y;
      return x;
    }
    //int main (void) { return 0 ; }
    
    c file icon wp_behav.c (1,145 bytes) 2012-04-16 12:02 +

-Relationships
+Relationships

-Notes

~0002933

virgile (developer)

The issue lies in the statement contract at line 62 of attached file: apparently Jessie (the compiler, not the plugin) does not support behavior with assumes clauses in this case.
+Notes

-Issue History
Date Modified Username Field Change
2012-04-16 12:02 nmuller New Issue
2012-04-16 12:02 nmuller Status new => assigned
2012-04-16 12:02 nmuller Assigned To => virgile
2012-04-16 12:02 nmuller File Added: wp_behav.c
2012-04-17 17:51 virgile Note Added: 0002933
2012-04-17 17:51 virgile Assigned To virgile => cmarche
2012-04-17 17:51 virgile Severity minor => feature
2012-04-17 17:51 virgile Reproducibility have not tried => always
2012-04-17 17:51 virgile Category Kernel > ACSL implementation => Plug-in > jessie
2012-04-17 17:51 virgile Product Version Frama-C Carbon-20110201 => Frama-C Hydrogen-20080301
2012-04-17 22:12 yakobowski Product Version Frama-C Hydrogen-20080301 => Frama-C Nitrogen-20111001
+Issue History