Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:37 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001027Frama-CKernel > ACSL implementationpublic2014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001027: incompatible types for a correct spec
DescriptionOn the attached file, we get:

$ frama-c -jessie max_ok.c
<snip>
File "max_ok.jc", line 53, characters 11-17: typing error: incompatible types: intP[..] and integer

Note that the WP plug-in proves this program correct wrt its spec.
TagsNo tags attached.
Attached Files
  • c file icon max_ok.c (428 bytes) 2011-11-25 18:34 -
    /*@
     requires \valid(i);
     requires \valid(j);
     requires \valid(r);
     assigns *r;
     behavior normal:
    	assumes r;
    	assigns *r;
    	ensures *j <= \at(*r,Here) && *i <= \at(*r,Here);
    	ensures \at(*r,Here) == *j || \at(*r,Here) == *i ;
    	ensures \result == 0;
     behavior r_null:
    	assumes !r;
    	assigns \nothing;
    	ensures \result == -1;
    */
    int max(int *r, int* i, int* j) { 
      if (!r) return -1; 
      *r = (*i < *j) ? *j : *i; 
      return 0; 
    } 
    
    c file icon max_ok.c (428 bytes) 2011-11-25 18:34 +

-Relationships
+Relationships

-Notes

~0002508

virgile (developer)

Arguably, the type-checker should transform assumes r into assumes r != (int *)0 or assumes r != \null instead of simply assumes r != 0 (similarly for assumes !r).

~0004691

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-11-25 18:34 signoles New Issue
2011-11-25 18:34 signoles Status new => assigned
2011-11-25 18:34 signoles Assigned To => cmarche
2011-11-25 18:34 signoles File Added: max_ok.c
2011-11-28 09:39 virgile Note Added: 0002508
2011-11-28 09:39 virgile Assigned To cmarche => virgile
2011-11-28 09:39 virgile Status assigned => confirmed
2011-11-28 09:39 virgile Category Plug-in > jessie => Kernel > ACSL implementation
2012-01-06 13:20 svn
2012-01-06 13:20 svn Status confirmed => resolved
2012-01-06 13:20 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:11 Source_changeset_attached => framac master 06b8e72d
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 06b8e72d
2014-02-12 16:58 Note Added: 0004691
2014-02-12 16:58 Status closed => resolved
+Issue History