--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on July 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why does a string literal not satisfy valid_read_string?



Hello again,

  I possibly silly question. The the code below - I get an unproved VC 
for the precondition of the call to "d2".  So.. why is a string literal 
not considered to satisfy "valid_read_string"?? I am using Frama-C 19...

Thanks,

  Rod


#include <string.h>

/*@ requires valid_read_string(s);
   @ assigns \nothing;
   @*/
int d2(const char *s);

int main(void)
{
   return d2 ("Hello rod");
}

The undischarged VC shows up as:

Goal Instance of 'Pre-condition'
  (call 'd2'):
Assume { (* Heap *) Have: linked(µ:Malloc at L1) /\ sconst(µ:Mchar at L1). }
Prove: P_valid_read_string(µ:Malloc at L1, µ:Mchar at L1, « global(Str_1) + 0 »).

--------------------------------------------------------------------------------
Prover Alt-Ergo: Unknown (103ms).


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190718/3e3daecf/attachment.html>