2021-01-15 15:05 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001908Frama-CPlug-in > Evapublic2015-03-17 22:18
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001908: Non terminating call to stncpy
DescriptionI get a NON TERMINATING FUNCTION on the attached example due to a call to strncpy, but I don't really understand why...

I added a \from part to the assigns property to remove the :

    warning: no \from part for clause 'assigns

But it was not the problem.

The message are:
    no state left in which to evaluate postcondition

I didn't even found a workaround :-(
Steps To Reproduce$ frama-c -val strncpy.c -cpp-extra-args="-I$(frama-c -print-share-path)/libc" -
val-builtin strlen:Frama_C_strlen
TagsNo tags attached.
Attached Files
  • c file icon strncpy.c (615 bytes) 2014-08-08 17:14 -
    // frama-c -val strncpy.c -cpp-extra-args="-I$(frama-c -print-share-path)/libc" -val-builtin strlen:Frama_C_strlen
    
    #include <string.h>
    
    //@ assigns dest[0..n-1] \from src[0..n-1];
    char * strncpy (char * dest, char const * src, size_t n);
    
    struct truc { char name[10]; } obj;
    
    int main (void) {
      struct truc * p = &obj;
      char name [] = "toto";
      size_t n = strlen(name);
    
      //@ assert a_n: n == 4;
      //@ assert a_name: \valid_read (name + (0..n));
      //@ assert a_rw_name: \valid (name + (0..n));
      //@ assert a_name_str: valid_string (name+0);
    
       strncpy(p->name, name, n);
       p->name[n] = '\0';
    
       return 0;
    }
    
    c file icon strncpy.c (615 bytes) 2014-08-08 17:14 +

-Relationships
+Relationships

-Notes

~0005404

yakobowski (manager)

Actually, the missing \from clauses are the culprit. Even with your addition, 'assigns \result \from dest' is still missing. Without it, '\result' gets assigned a default value that makes the postcondition '\result == dest' completely invalid.

I will harden the message about '\from' clauses further, so that it also detects missing '\return' clauses. Concerning string.h, a patch that adds all the missing 'assigns' would be gladly accepted.

~0005406

Anne (reporter)

I am very sorry : I should have noticed that ! :-(

About string.h, I'll have a look at it.

~0005475

yakobowski (manager)

Fix committed to master branch.
+Notes

-Issue History
Date Modified Username Field Change
2014-08-08 17:14 Anne New Issue
2014-08-08 17:14 Anne Status new => assigned
2014-08-08 17:14 Anne Assigned To => yakobowski
2014-08-08 17:14 Anne File Added: strncpy.c
2014-08-08 21:09 yakobowski Note Added: 0005404
2014-08-11 08:14 Anne Note Added: 0005406
2014-09-19 16:32 yakobowski Source_changeset_attached => framac master 3935a098
2014-09-19 16:32 yakobowski Note Added: 0005475
2014-09-19 16:32 yakobowski Status assigned => resolved
2014-09-19 16:32 yakobowski Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History