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

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001587Frama-CPlug-in > wppublic2014-06-12 12:53
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001587: syntax error for alt-ergo with memset spec
DescriptionWhen trying to prove the first loop invariant of this example, there is a message:

/tmp/wpd57f12.dir/typed/A_MemSet.ergo:10:[wp] user error:
Prover Alt-Ergo returns Failed
characters 6-106:typing error: syntax error

and neither the establishment nor the preservation can be proved.
Additional InformationCommand line is :
frama-c -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c -wp
TagsNo tags attached.
Attached Files
  • c file icon pb_wp.c (609 bytes) 2013-12-16 12:15 -
    // frama-c-gui -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c
    #include <string.h>
    
    //@ assigns \result \from *X;
    size_t size(char *X);
    
    //@ requires \valid (buf + (0 .. buflen-1));
    int write ( const char *X, unsigned char *buf, size_t buflen )
    {
        size_t i, j, n;
    
        n = size( X );
        if( buflen < n ) return( 1 );
    
        memset( buf, 0, buflen );
    
        //@ ghost size_t n0 = n;
       
        /*@ loop invariant 0 <= n <= n0; 
            loop invariant j == n0 - n; 
    	loop invariant i == buflen - 1 - j;
    	*/
        for( i = buflen - 1, j = 0; n > 0; i--, j++, n-- )
            buf[i] = 1;
    
        return( 0 );
    }
    
    
    c file icon pb_wp.c (609 bytes) 2013-12-16 12:15 +

-Relationships
+Relationships

-Notes

~0004379

correnson (manager)

@Anne : merci pour le rapport de bug !
L.

~0004385

correnson (manager)

Fix committed to master branch.

~0004543

correnson (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-12-16 12:15 Anne New Issue
2013-12-16 12:15 Anne Status new => assigned
2013-12-16 12:15 Anne Assigned To => correnson
2013-12-16 12:15 Anne File Added: pb_wp.c
2013-12-17 13:03 svn
2013-12-17 13:03 svn Status assigned => resolved
2013-12-17 13:03 svn Resolution open => fixed
2013-12-17 13:03 correnson Note Added: 0004379
2013-12-19 01:11 correnson Source_changeset_attached => framac master d29159c3
2014-01-06 14:20 correnson Source_changeset_attached => framac master 52561248
2014-01-06 14:20 correnson Note Added: 0004385
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon 52561248
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon d29159c3
2014-02-12 16:57 correnson Note Added: 0004543
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2014-06-12 12:53 correnson Relationship added has duplicate 0001806
2014-06-12 12:55 correnson Relationship deleted has duplicate 0001806
+Issue History