Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Alt Ergo - Problem

  • Subject: [Frama-c-discuss] Alt Ergo - Problem
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sat, 3 Oct 2015 14:32:07 -0400
  • In-reply-to: <561000C3.2020700@gmail.com>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C766044995@Mail1.FCMD.local> <52D1556E.7010400@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76604499E@Mail1.FCMD.local> <52D15C30.40602@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB78@Mail1.FCMD.local> <52D15D7F.3000800@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB79@Mail1.FCMD.local> <52D16266.3040201@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB7A@Mail1.FCMD.local> <52D16676.3000200@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB7B@Mail1.FCMD.local> <52D16727.8030804@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7660449A2@Mail1.FCMD.local> <52D4D24E.8060007@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DC58@Mail1.FCMD.local> <52D55374.8020404@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682E584@Mail1.FCMD.local> <52EF36F1.7020100@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB147@Mail1.FCMD.local> <561000C3.2020700@gmail.com>
Hi all,

I'm having problem in validating an assert which is true at run-time (at least on my machine) but alt-ergo is not happy with my commented assert, not sure why? I checked with an alt-ergo expert, his response is given below.

#include <stdio.h>
#include <assert.h>

int main()
{
  int x = (1 << 16)-1; /* two power 16 - 1 */

  // why is this not ok?

  /*@ assert x*x < 0 ;*/

  assert(x*x < 0); /* This is true when I run using gcc and then a.out */ }

frama-c -wp -wp-rte square_neg.c -wp-no-check -wp-no-simpl -wp-print -wp-model "Typed,var,cint,real" -wp-no-let -wp-no-pruning -wp-no-clean -wp-no-bits

Goal Assertion (file square_neg.c, line 10):
Assume {
  (* Domain *)
  Type: (is_sint32 x_0).
  (* Block In *)
  Have: ta_retres_0 /\ ta_x_0 /\ (not ta_retres_2) /\ (not ta_x_2).
  (* square_neg.c:6: Assignment *)
  Have: x_0=(to_sint32 ((to_sint32 (lsl 1 16))-1)).
}
Prove: (x_0*x_0)<0.
Prover Alt-Ergo returns Unknown

-----Original Message-----
From: Mohamed Iguernlala [mailto:mohamed.iguernelala at gmail.com]
Sent: Saturday, October 03, 2015 12:22 PM
To: Dharmalingam Ganesan
Subject: Re: Alt Ergo - Problem

Hi Dharmalingam,

I think this is rather a problem in WP plugin. In fact, one hypothesis in the goal says that x_0 fits in
32 bits (Type: (is_sint32 x_0)), but there is nothing that states that
(x_0*x_0) should be a 32-bits integer.

So for gcc, i * i = 65535*65535 overflows on 32 bits, but for Alt-Ergo, which works on mathematical integers, i * i = 65535*65535 = 4294836225.

A hypothesis (is_sint32 (x_0*x_0)) is missing in the VC generated by WP.

Mohamed.

Goal Assertion (file square_neg.c, line 10):
Assume {
   (* Domain *)
   Type: (is_sint32 x_0).
   (* Block In *)
   Have: ta_retres_0 /\ ta_x_0 /\ (not ta_retres_2) /\ (not ta_x_2).
   (* square_neg.c:6: Assignment *)
   Have: x_0=(to_sint32 ((to_sint32 (lsl 1 16))-1)).
}
Prove: (x_0*x_0)<0.
Prover Alt-Ergo returns Unknown



Le 02/10/2015 20:44, Dharmalingam Ganesan a écrit :
> Hi Mohamed,
>
> How are you doing? I'm having problem in validating an assert which is true at run-time (at least on my machine) but alt-ergo is not happy with my commented assert, not sure why?
>
> #include <stdio.h>
> #include <assert.h>
>
> int main()
> {
>    int x = (1 << 16)-1; /* two power 16 - 1 */
>
>    // why is this not ok?
>
>    /*@ assert x*x < 0 ;*/
>
>    assert(x*x < 0); /* This is true when I run using gcc and then
> a.out */ }
>
> frama-c -wp -wp-rte square_neg.c -wp-no-check -wp-no-simpl -wp-print
> -wp-model "Typed,var,cint,real" -wp-no-let -wp-no-pruning -wp-no-clean
> -wp-no-bits
>
> Goal Assertion (file square_neg.c, line 10):
> Assume {
>    (* Domain *)
>    Type: (is_sint32 x_0).
>    (* Block In *)
>    Have: ta_retres_0 /\ ta_x_0 /\ (not ta_retres_2) /\ (not ta_x_2).
>    (* square_neg.c:6: Assignment *)
>    Have: x_0=(to_sint32 ((to_sint32 (lsl 1 16))-1)).
> }
> Prove: (x_0*x_0)<0.
> Prover Alt-Ergo returns Unknown
>
>
> -----Original Message-----
> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
> Behalf Of Mohamed Iguernelala
> Sent: Monday, February 03, 2014 1:28 AM
> To: Dharmalingam Ganesan
> Subject: Re: Alt Ergo - Problem
>
> Hello,
>
> No, we have not considered fixing it yet.
>
> - Mohamed.
>
> Le 03/02/2014 01:22, Dharmalingam Ganesan a écrit :
>> Hi Mohamed,
>>
>> Thanks. Just curious whether there is a fix for this issue I can test for.
>>
>> Best regards,
>> Dharma
>>
>> -----Original Message-----
>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>> Behalf Of Mohamed Iguernelala
>> Sent: Tuesday, January 14, 2014 10:11 AM
>> To: Dharmalingam Ganesan
>> Subject: Re: Alt Ergo - Problem
>>
>> The code generated for Alt-Ergo is valid. But, our solver spends a lot of time during "triggers inference": a step that is coupled with type-checking. We'll try to fix that soon.
>>
>> Anyway, this does not explain the -7 UNIX signal.
>>
>> - Mohamed.
>>
>> Le 14/01/2014 14:29, Dharmalingam Ganesan a écrit :
>>> Hi Mohamed,
>>>
>>> OK. Thanks a lot for trying the example. Is it Frama-c that generates "invalid" code for Alt-Ergo to get it lost in the type-checking phase?
>>>
>>> Thanks,
>>> Dharma
>>>
>>> -----Original Message-----
>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>> Behalf Of Mohamed Iguernelala
>>> Sent: Tuesday, January 14, 2014 1:00 AM
>>> To: Dharmalingam Ganesan
>>> Subject: Re: Alt Ergo - Problem
>>>
>>> Hi,
>>>
>>> I tried you example yesterday evening. Alt-Ergo is lost in the type-checking phase in which it takes 8 minutes and It says "I don't know" after type-checking.
>>>
>>> However, I don't think Alt-Ergo is responsible for the -7 signal, since we never exit with such a signal.I don't think that OCaml is responsble too in case of some crash.
>>>
>>> - Mohamed.
>>>
>>> Le 13/01/2014 16:29, Dharmalingam Ganesan a écrit :
>>>> Hi Mohamed,
>>>>
>>>> Here is the mlw file for the other issue related to the UNIX signal.
>>>>
>>>> Let me know if this helps for your debugging.
>>>>
>>>> If you badly need the C code, I will try to do sanitize before sending out to avoid any problems.
>>>>
>>>> Thanks,
>>>> Dharma
>>>> ________________________________________
>>>> From: iguernelala mohamed [mohamed.iguernelala at gmail.com] On Behalf
>>>> Of Mohamed Iguernelala [mohamed.iguernelala at ocamlpro.com]
>>>> Sent: Saturday, January 11, 2014 10:45 AM
>>>> To: Dharmalingam Ganesan
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>> I would like to simplify the code to get a minimal C program for which the bevaviour of Oxygen and Fluorine is different.
>>>>
>>>> Le 11/01/2014 16:43, Dharmalingam Ganesan a écrit :
>>>> I think the code is correct. As you can see the variables I refer in the basic behavior are never updated after the first if-else block, although the code is somewhat complex.
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>> Behalf Of Mohamed Iguernelala
>>>> Sent: Saturday, January 11, 2014 10:43 AM
>>>> To: Dharmalingam Ganesan
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>> So you think your code is correct or incorrect ?
>>>>
>>>> Le 11/01/2014 16:26, Dharmalingam Ganesan a écrit :
>>>> Ok, great, thanks for your input. Yes, that's my Bio.
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>> Behalf Of Mohamed Iguernelala
>>>> Sent: Saturday, January 11, 2014 10:25 AM
>>>> To: Dharmalingam Ganesan
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>> Le 11/01/2014 16:07, Dharmalingam Ganesan a écrit :
>>>> Fully Agree. I hope I will get some help from Frama-c developers on
>>>> this issue. I had some good plans for formal verification. Sounds the path is not easy... Sure, they are more competent on Frama-C, as I only work on Alt-Ergo.
>>>>
>>>>
>>>>      Will it be possible to know what kind of C code will let A-E says unable to prove and/or need more assistance from the user.
>>>> In which context you are working ? Your are using integers ? floats ? If you feel that you need a support on Alt-Ergo, don't hesitate to contact an OCamlPro representative.
>>>>
>>>>
>>>>
>>>>      The code I'm currently targeting has no loops because it has real-time timer that calls periodically. I think it is good - no loop invariants to worry. Anything else I must be aware of?
>>>> Yea. This should be a quite simple code. The other important thing is aliasing. I don't how Frama-C handles this point.
>>>>
>>>> BTW, is this your bio ?
>>>> http://cp.mcafee.com/d/k-Kr6x8SyMMOYYqemnQPtPqtTAnC67QkPqtTAnC67T6j
>>>> qtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISeJuZQn7-LP
>>>> dTXCzBNctRXBTATevd7bXxEVop7th5dqWqJXLYG7DR8OJMddECS3t-pjh7npujsKrKr
>>>> 01SmVmSK__bUxwK1d1yMEj0xYp2o3Q0FAk9xwI1Mf42Ey850sI1NIrbBxa8y1g7b0sr
>>>> 6OUj31JmFflvgWh5LUMY_jZ1h4jVsSC-qejhOUr1vF6y0gfCq81G96FEwbCy0bhGgfZ
>>>> kSCCrVIhW
>>>> r
>>>> j
>>>> KYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCQTQQ644T-LOt
>>>> Q
>>>> S
>>>> k
>>>> TXZuVt4sMzPdTTHEIYJt6OaaJXLYG7DR8OJMddECS3t-hojuv78I9CzATsS03R0PIbu
>>>> x
>>>> Y
>>>> 2
>>>> cEvYpg8YSGxTEdUXJCPVBIg9X5njVg8WGn8X3Wr0Qu00XbsHrnv_BYgNce1omG0XOq8
>>>> 4
>>>> f
>>>> z
>>>> 8j0uwqW6ygEczb09Ec1QMO-6gYf0B-MM7j3bUp3MY2go830tccLxAf3M9vc30tccE1w
>>>> 1
>>>> A
>>>> U
>>>> xxo2bywqWbxJOE3l0E91Um5wAerc34pxI3O8p0wZAaAoE2gEcwN06fEE2En0VoK7j39
>>>> y
>>>> o
>>>> b
>>>> 0op0s1MiUS8H6hTIxTGwkabfE7K0ceQf384OI5Wcy8Iqeg8c0AO80c2gGS1830A2Ewl
>>>> 6
>>>> W
>>>> 8
>>>> 2C5xxYaAiWbxlQLoqoryuh0o1T0fco2OM730MYM19obyU76C9DA12ou1a1y9Ui4gn01
>>>> _
>>>> 4
>>>> 2
>>>> siZDng75i9kCMnwwa1s4AN50M5g752tTxMmgoK2S1gG0V5Yb4XLzgbu75MB42Ewhe04
>>>> C
>>>> z
>>>> U
>>>> SHkDGLEt8yTYouvF-wEy9YKrhd7bxEVpdwLQzh087Pd40R4zkQg5Ph05ER87-GrKrly
>>>> 6
>>>> V
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>> Behalf Of Mohamed Iguernelala
>>>> Sent: Saturday, January 11, 2014 10:05 AM
>>>> To: Dharmalingam Ganesan
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>> It is better to use the latest versions of tools I think, to benefit from latest bugfixes.
>>>>
>>>>
>>>> Le 11/01/2014 16:01, Dharmalingam Ganesan a écrit :
>>>> Sorry. I just got confused. Yes, we both get I don't know.
>>>>
>>>> I much work will let take to fix the syntax errors for me if I switch to the Oxygen version temporarily?
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>> Behalf Of Mohamed Iguernelala
>>>> Sent: Saturday, January 11, 2014 9:59 AM
>>>> To: Dharmalingam Ganesan
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>> So, you get I don't know :-)
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> File "foo_F.mlw", line 306, characters 1-2211:I don't know
>>>>
>>>> Le 11/01/2014 15:57, Dharmalingam Ganesan a écrit :
>>>>
>>>> File "foo_F.mlw", line 306, characters 1-2211:I don't know
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> ________________________________________
>>>>
>>>> From: iguernelala mohamed
>>>> [mohamed.iguernelala at gmail.com<mailto:mohamed.iguernelala at gmail.com
>>>> >
>>>> ]
>>>> On Behalf Of Mohamed Iguernelala
>>>> [mohamed.iguernelala at ocamlpro.com<mailto:mohamed.iguernelala at ocamlpro.
>>>> com>]
>>>>
>>>> Sent: Saturday, January 11, 2014 9:30 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> foo_F.mlw : generated by Fluorine. A-E says "I don't know"
>>>>
>>>> foo_O.mlw : generated by Oxygen. A-E says "Valid"
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 15:28, Dharmalingam Ganesan a écrit :
>>>>
>>>> OK, I'm somewhat unlucky then.
>>>>
>>>>
>>>>
>>>> Do you mind sending me the Fluroine generated mlw file, if possible?
>>>>
>>>>
>>>>
>>>> -----Original Message-----
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>> Behalf Of Mohamed Iguernelala
>>>>
>>>> Sent: Saturday, January 11, 2014 9:26 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> The syntax error is in the VC generated by Frama-C Oxygen. Frama-C Fluorine generated a syntactically correct VC for alt-ergo 0.95.2.
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 15:23, Dharmalingam Ganesan a écrit :
>>>>
>>>> Yes, I did run it on /usr/local/bin/alt-ergo, as shown in previous email.
>>>>
>>>>
>>>>
>>>> Which syntax errors did you fix?
>>>>
>>>>
>>>>
>>>> -----Original Message-----
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>>
>>>> Behalf Of Mohamed Iguernelala
>>>>
>>>> Sent: Saturday, January 11, 2014 9:21 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> You have run on alt-ergo on it:
>>>>
>>>>
>>>>
>>>> $ /usr/local/bin/alt-ergo /home/dharma/foo_basic_post_Alt-Ergo.mlw
>>>>
>>>>
>>>>
>>>> Alt-Ergo says that it does'nt know if the goal is valid.
>>>>
>>>> - Either Frama-C generated a non valid VC and the answer of
>>>> Alt-Ergo
>>>>
>>>> is correct
>>>>
>>>> - Or the goal is valid but alt-ergo is not able to prove it. But
>>>> this
>>>>
>>>> is a little bit surprising because Alt-Ergo proves the goal
>>>> generated
>>>>
>>>> by Frama-C Oxygen (after fixing syntax errors)
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 15:12, Dharmalingam Ganesan a écrit :
>>>>
>>>> Yes, I have a file in $HOME. I attach for you.
>>>>
>>>>
>>>>
>>>> [formal_verification]$ /usr/local/bin/alt-ergo
>>>>
>>>> /home/dharma/foo_basic_post_Alt-Ergo.mlw
>>>>
>>>> File "/home/dharma/foo_basic_post_Alt-Ergo.mlw", line 306,
>>>> characters
>>>>
>>>> 1-2211:I don't know
>>>>
>>>>
>>>>
>>>> How do fix/run?
>>>>
>>>> ________________________________________
>>>>
>>>> From: iguernelala mohamed
>>>> [mohamed.iguernelala at gmail.com<mailto:mohamed.iguernelala at gmail.com
>>>> >
>>>> ]
>>>> On Behalf
>>>>
>>>> Of Mohamed Iguernelala
>>>> [mohamed.iguernelala at ocamlpro.com<mailto:mohamed.iguernelala at ocamlpro.
>>>> com>]
>>>>
>>>> Sent: Saturday, January 11, 2014 9:11 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> Oh yeah ! You are right. Both are accepted by Alt-Ergo. The file
>>>>
>>>> given by Frama-C have extension .mlw
>>>>
>>>>
>>>>
>>>> So there is a .mlw generated in $HOME.
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 15:09, Dharmalingam Ganesan a écrit :
>>>>
>>>> Yes. I have only one terminal. I think the "dummy" alt-ergo is indeed called but the first arg is .mlw but not .why.
>>>>
>>>>
>>>>
>>>> -----Original Message-----
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>>
>>>> Behalf Of Mohamed Iguernelala
>>>>
>>>> Sent: Saturday, January 11, 2014 9:09 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> No. You are doing all the manipulations in the same terminal ?
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 15:07, Dharmalingam Ganesan a écrit :
>>>>
>>>> I'm on 64-bit Ubuntu Linux machine. Will that be a problem?
>>>>
>>>>
>>>>
>>>> -----Original Message-----
>>>>
>>>> From: iguernelala mohamed [mailto:mohamed.iguernelala at gmail.com] On
>>>>
>>>> Behalf Of Mohamed Iguernelala
>>>>
>>>> Sent: Saturday, January 11, 2014 9:07 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> On both Oxygen and Flourine. And this worked for both.
>>>>
>>>>
>>>>
>>>> I don't understand why this is not working for you.
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>            Le 11/01/2014 15:04, Dharmalingam Ganesan a écrit :
>>>>
>>>> You did this trick on Flourine version of frama-c, right?
>>>>
>>>>
>>>>
>>>> [formal_verification]$ frama-c -version
>>>>
>>>> Version: Fluorine-20130601
>>>>
>>>> Compilation date: Tue Jan 7 20:36:30 EST 2014 Share path:
>>>>
>>>> /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE
>>>>
>>>> variable) Library path: /usr/local/lib/frama-c (may be overridden
>>>>
>>>> with FRAMAC_LIB variable) Plug-in paths:
>>>>
>>>> /usr/local/lib/frama-c/plugins (may be overridden with
>>>>
>>>> FRAMAC_PLUGIN
>>>>
>>>> variable) ________________________________________
>>>>
>>>> From: iguernelala mohamed
>>>> [mohamed.iguernelala at gmail.com<mailto:mohamed.iguernelala at gmail.com
>>>> >
>>>> ]
>>>> On
>>>>
>>>> Behalf Of Mohamed Iguernelala
>>>> [mohamed.iguernelala at ocamlpro.com<mailto:mohamed.iguernelala at ocamlpro.
>>>> com>]
>>>>
>>>> Sent: Saturday, January 11, 2014 9:01 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> and you have no .why file in $HOME ?
>>>>
>>>>
>>>>
>>>> What dit the command which alt-ergo return ?
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 15:00, Dharmalingam Ganesan a écrit :
>>>>
>>>> Yes. I did.
>>>>
>>>>
>>>>
>>>> [wp] Running WP plugin...
>>>>
>>>> [wp] Collecting axiomatic usage
>>>>
>>>> [rte] annotating function foo
>>>>
>>>> [wp] 1 goal scheduled
>>>>
>>>> [wp] [Alt-Ergo] Goal typed_foo_basic_post : Failed
>>>>
>>>>                 Error: Can not understand Alt-Ergo output.
>>>>
>>>>
>>>>
>>>> ________________________________________
>>>>
>>>> From: iguernelala mohamed
>>>> [mohamed.iguernelala at gmail.com<mailto:mohamed.iguernelala at gmail.com
>>>> >
>>>> ]
>>>> On
>>>>
>>>> Behalf Of Mohamed Iguernelala
>>>> [mohamed.iguernelala at ocamlpro.com<mailto:mohamed.iguernelala at ocamlpro.
>>>> com>]
>>>>
>>>> Sent: Saturday, January 11, 2014 8:59 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> Have you tried to remove "echo "First arg:$1"" ?
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 14:55, Dharmalingam Ganesan a écrit :
>>>>
>>>> Very, very clear.
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> [formal_verification]$ cat alt-ergo echo "First arg:$1"
>>>>
>>>> cp $1 $HOME
>>>>
>>>>
>>>>
>>>> I tried your trick but got this output below. Never got a why file, unfortunately.
>>>>
>>>>
>>>>
>>>> [formal_verification]$ frama-c -wp -wp-rte -lib-entry -main foo
>>>>
>>>> foo.c -wp-bhv=basic -wp-out t [kernel] preprocessing with "gcc -C -E -I.  foo.c"
>>>>
>>>> [wp] Running WP plugin...
>>>>
>>>> [wp] Collecting axiomatic usage
>>>>
>>>> [rte] annotating function foo
>>>>
>>>> [wp] 1 goal scheduled
>>>>
>>>> ------------------------------------------------------------
>>>>
>>>> --- Alt-Ergo (stdout) :
>>>>
>>>> ------------------------------------------------------------
>>>>
>>>> First arg:t/typed/foo_basic_post_Alt-Ergo.mlw
>>>>
>>>> ------------------------------------------------------------
>>>>
>>>> [wp] [Alt-Ergo] Goal typed_foo_basic_post : Failed
>>>>
>>>>                  Error: Can not understand Alt-Ergo output.
>>>>
>>>>
>>>>
>>>> ________________________________________
>>>>
>>>> From: iguernelala mohamed
>>>> [mohamed.iguernelala at gmail.com<mailto:mohamed.iguernelala at gmail.com
>>>> >
>>>> ]
>>>> On
>>>>
>>>> Behalf Of Mohamed Iguernelala
>>>> [mohamed.iguernelala at ocamlpro.com<mailto:mohamed.iguernelala at ocamlpro.
>>>> com>]
>>>>
>>>> Sent: Saturday, January 11, 2014 8:42 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> Frama-C generates a file xxx.why for Alt-Ergo but it deletes it at exit.
>>>>
>>>> I don't how to say to Frama-C to keep this file. So:
>>>>
>>>>
>>>>
>>>> 1) I created a dummy alt-ergo that just copies the file xxx.why
>>>>
>>>> it is given to $HOME
>>>>
>>>> 2) I added it to the path to hide the right alt-ergo
>>>>
>>>> 2) I executed Frama-C with the dummy alt-ergo
>>>>
>>>> 3) I obtained a file xxx.why in my $HOME that I can give to the
>>>>
>>>> right alt-ergo and/or modify
>>>>
>>>>
>>>>
>>>> - Mohamed.
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 14:37, Dharmalingam Ganesan a écrit :
>>>>
>>>> Sorry, I'm not following you. Did you convert my C code to alt-ergo by hand, I hope not, to proof the "basic" behavior?
>>>>
>>>>
>>>>
>>>> I guess my question is how did you generate "store_foo_basic_post_po_ergo.why"
>>>>
>>>>
>>>>
>>>> -----Original Message-----
>>>>
>>>> From: iguernelala mohamed
>>>>
>>>> [mailto:mohamed.iguernelala at gmail.com]
>>>>
>>>> On Behalf Of Mohamed Iguernelala
>>>>
>>>> Sent: Saturday, January 11, 2014 8:34 AM
>>>>
>>>> To: Dharmalingam Ganesan
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> I used a "dummy" alt-ergo that is just a script which copy its argument to $HOME.
>>>>
>>>>
>>>>
>>>> $ cat alt-ergo
>>>>
>>>> cp $1 $HOME
>>>>
>>>>
>>>>
>>>> I then used the right alt-ergo on the copied file. Sorry, I'm
>>>>
>>>> not a Frama-c expert :-)
>>>>
>>>>
>>>>
>>>> - Mohamed.
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Le 11/01/2014 14:30, Dharmalingam Ganesan a écrit :
>>>>
>>>> Thanks a lot Mohammed. I'm sorry that I sent that email to your group.
>>>>
>>>>
>>>>
>>>> BTW: How did you get the why file generated, as mentioned on the stack overflow?
>>>>
>>>>
>>>>
>>>> Alt-Ergo -version show 0.95.2; Frama-c -version shows
>>>>
>>>> Fluorine-20130601
>>>>
>>>>
>>>>
>>>> -----Original Message-----
>>>>
>>>> From: iguernelala mohamed
>>>>
>>>> [mailto:mohamed.iguernelala at gmail.com]
>>>>
>>>> On Behalf Of Mohamed Iguernelala
>>>>
>>>> Sent: Saturday, January 11, 2014 8:21 AM
>>>>
>>>> To: Dharmalingam Ganesan;
>>>> alt-ergo at ocamlpro.com<mailto:alt-ergo at ocamlpro.com>
>>>>
>>>> Subject: Re: Alt Ergo - Problem
>>>>
>>>>
>>>>
>>>> Hello,
>>>>
>>>>
>>>>
>>>> I have just answered your question on stackovervflow to enable interaction with people developping frama-c.
>>>>
>>>>
>>>>
>>>> BTW, it's better to ask questions on frama-c-discuss[1] or on alt-ergo-beginners[1] lists. alt-ergo at ocamlpro.com<mailto:alt-ergo at ocamlpro.com> is not intended for that.
>>>>
>>>>
>>>>
>>>> Regards,
>>>>
>>>>
>>>>
>>>> [1]
>>>>
>>>> http://cp.mcafee.com/d/1jWVIqdEIccLf6zBBZcTsSDtV5VxxZ5cSDtV5VxxZNAS
>>>> DtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdzHnLt5N_HYP
>>>> t-VEVsj7tuVtVdPDPhO-Uqem6hTkhjmKCHuX_axVZicHs3jqpJwTvCkQhRSnATbCXCM
>>>> 0tBKlJHL_O-8pFC20EZgQsFAM8v6gC0Z0STSs51CM9Ec1QMO-6gYf0B-MM76RqAZlZ3
>>>> F4m_z3PZfQ54hfBPqrVEVd7bxI5-Aq810-pEw6EAqCy0Kq80J6F0_RjqqpJiEsqgcd
>>>>
>>>> t
>>>>
>>>> V5
>>>>
>>>> V
>>>>
>>>> xxZN
>>>>
>>>> ASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdA7TS
>>>>
>>>> 4
>>>>
>>>> k4
>>>>
>>>> T
>>>>
>>>> -LPP
>>>>
>>>> ObZQuLsKCy_vAmnANPX7bnhIyyHsQsKsG7DR8OJMddECSjt-jLuZXTLuVKVI06
>>>>
>>>> v
>>>>
>>>> aA
>>>>
>>>> W
>>>>
>>>> sht0
>>>>
>>>> 0_QEhBLeNMjlS67OFek7qUX7ltbSbEiFpKB3qJiuG-xQybvNxV-DW2y8DOVJyX
>>>>
>>>> x EV d wLQz h087Pd40R4zkQg5Ph05ER87-GrKrOnhmSBRfoxeb
>>>>
>>>> [2]
>>>>
>>>> http://cp.mcafee.com/d/k-Kr40Uq43qb33bPNEVpvjdTdFTuhuoovhjdFTuhuoov
>>>> spdFTuhuoovhodFTujsKMCYCrg8X3Wr05eSbGEsSGxTEdCTr5RkerlgXQ6PoWRXThsv
>>>> W_cTvKqen4NTnKnujsVYQsLK6zBxAtR4kRHFGTK_OEuvkzaT0QSOrodTVBd4ttBVdOV
>>>> KVI07prBrqX_YLy6fKxsi1BNpwk5y1063gpHmBk1SH0k6g8Y1wMg2Pb82WI17wcrlGj
>>>> RnQeAhr-cffQ_gkh4-ndFLCzAQsK6MnWhEw43VCy0qyhGq82VEw2QqA3_ldFFCM-CoK
>>>> x4a
>>>>
>>>> O
>>>>
>>>> bP
>>>>
>>>> 3
>>>>
>>>> 3Xz9
>>>>
>>>> JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSr8fLI8
>>>>
>>>> E
>>>>
>>>> 9L
>>>>
>>>> Z
>>>>
>>>> vDDA
>>>>
>>>> nXEZuVtd5-_8IL9zDSemKzp55mVEVsVkffGhBrwqrjdICXYDuZXTLuZPtPo0c-
>>>>
>>>> l
>>>>
>>>> 9Q
>>>>
>>>> W
>>>>
>>>> JJlf
>>>>
>>>> Vqds4RtxxYGjB1SKqvcLYidiV3OcEg-d3qJiuG-xQybvNxV-DW2y8DOVJyXxEV
>>>>
>>>> d
>>>>
>>>> wL
>>>>
>>>> Q
>>>>
>>>> zh08
>>>>
>>>> 7Pd40R4zkQg5Ph05ER87-GrKrUiIdcUFQ
>>>>
>>>>
>>>>
>>>> Mohamed Iguernelala.
>>>>
>>>> Senior R&D Engineer, OCamlPro
>>>>
>>>> Research Associate, VALS team, LRI.
>>>>
>>>> http://cp.mcafee.com/d/FZsScygwd2hJ5xxBVUQsILFCXCQXL8LccfEFCQXL8Lcc
>>>> fKcCQXL8LccfEI6QXL9KnojujdE4txZdw2Dr5RkerlgXQ6PrJyWG7dGEtW3pItqZXEK
>>>> fZvCrLTd7byoXHTbL9Ks-qenT3hOMOeWyaqRQRrTvVkffGhBrwqrodI6XYOCyeKOYCV
>>>> sTsS03IJOJJt_-nN3dcMg57w7up9wg-cxc1W1JLIUa3dwjgo3FxBYcxUu1bZxwedGR9
>>>> WHW7i8J_67DWvEa8yvbCQTPhOqen3obZ8Qg21YPh0dh8Rd41sQg1qdi1_GCQQPoqRP6
>>>> TpQuy8t
>>>>
>>>> t
>>>>
>>>> V5
>>>>
>>>> V
>>>>
>>>> xxZN
>>>>
>>>> ASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdA7TS
>>>>
>>>> 4
>>>>
>>>> k4
>>>>
>>>> T
>>>>
>>>> -LPP
>>>>
>>>> ObZQuLsKCy_vAmnANPX7bnhIyyHsQsKsG7DR8OJMddICSjt-jLuZXTLuVKVI05
>>>>
>>>> 8
>>>>
>>>> yT
>>>>
>>>> Y
>>>>
>>>> uB1S
>>>>
>>>> FJmFflvgWh5LUMY_jZ1h4jVsSNtMQsCMnWhEw43VCy0qyhGq82VEw2QqA3_ldT
>>>>
>>>> d
>>>>
>>>> Fs
>>>>
>>>> q
>>>>
>>>> UVxA
>>>>
>>>> s
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Le 10/01/2014 20:14, Dharmalingam Ganesan a écrit :
>>>>
>>>> Hi,
>>>>
>>>>
>>>>
>>>> I'm using Alt-Ergo theorem prover via the Frama-c tool. I'm unable to figure out why prover is unable to validate the "basic" behavior defined below.
>>>>
>>>>
>>>>
>>>> The basic behavior is indeed valid from my manual inspection because the variable tenumRMode is only updated once in the first else statement, although the attached code is somewhat lengthy and complex.
>>>>
>>>>
>>>>
>>>> /*@
>>>>
>>>>                  @ behavior basic:
>>>>
>>>>                  @  assumes fRrValue == 0;
>>>>
>>>>                  @  ensures tenumRMode == SS_A_MODE;
>>>>
>>>>                  @
>>>>
>>>> */
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> [formal_verification]$ frama-c -wp -wp-rte -lib-entry -main
>>>>
>>>> foo foo.c -wp-bhv=basic [kernel] preprocessing with "gcc -C -E -I.  foo.c"
>>>>
>>>> [wp] Running WP plugin...
>>>>
>>>> [wp] Collecting axiomatic usage [rte] annotating function foo
>>>>
>>>> [wp] 1 goal scheduled [wp] [Alt-Ergo] Goal
>>>>
>>>> typed_foo_basic_post : Unknown (Qed:16ms)
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Any comments will help me.
>>>>
>>>>
>>>>
>>>> FYI: I ran frama-c (latest version) on Ubuntu with Unix 64-bit machine.
>>>>
>>>>
>>>>
>>>> Thanks,
>>>>
>>>> Dharma
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>