--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on July 2019 ---
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>