| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000926 | Frama-C | Plug-in > wp | public | 2011-08-15 17:53 | 2011-10-10 14:14 |
|
| Reporter | jessie_user | |
| Assigned To | correnson | |
| Priority | normal | Severity | major | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Carbon-20110201 | |
| Target Version | | Fixed in Version | Frama-C Nitrogen-20111001 | |
|
| Summary | 0000926: wp-plugin does not generate coq *.v goals. |
| Description | Wp plugin for carbon-20110201 does not generate coq proover goals.
In carbon-beta2 there is no such error.
frama-c -wp-help
Plug-in name: WP 0.3
frama-c -version
Version: Carbon-20110201
Ocaml-version: 64 bit, we have not GUI installed.
Example:
frama-c -wp -wp-out wp_longlong -wp-rte test_wp_longlong.c
ls wp_longlong/
store_add_assert_1_rte_body.txt store_add_assert_2_rte_head.txt store_add_post_1_A_body.txt
store_add_assert_1_rte_head.txt store_add_assert_3_rte_body.txt store_add_post_1_A_head.txt
store_add_assert_2_rte_body.txt store_add_assert_3_rte_head.txt store_env1.txt
There are no *.v coq-files.
Example with another options: (-wp-proof coq)
frama-c -wp -wp-out wp_longlong -wp-proof coq -wp-rte test_wp_longlong.c
wp_longlong Directory with goals to prove contains:
ls wp_longlong/
store_add_assert_1_rte_body.txt store_add_assert_2_rte_head.txt store_add_assert_3_rte_log.txt store_env1.txt wp.vo
store_add_assert_1_rte_head.txt store_add_assert_2_rte_log.txt store_add_post_1_A_body.txt store_env1.v
store_add_assert_1_rte_log.txt store_add_assert_3_rte_body.txt store_add_post_1_A_head.txt store_env1.vo
store_add_assert_2_rte_body.txt store_add_assert_3_rte_head.txt store_add_post_1_A_log.txt store_model.vo
There are no coq *.v files, only store_env1.v without goals to proof.
|
| Tags | No tags attached. |
|
| Attached Files |  test_wp_longlong.c [^] (251 bytes) 2011-08-15 17:53 [Show Content] [Hide Content]struct INTEGER32 {
// int value; // Ok
long long value; // Fails
};
typedef struct INTEGER32 int32;
/*@
requires \valid(x) && \valid(y);
ensures A: \valid(x);
*/
void add (int32* x, int32* y){
int32 erg;
erg.value = x->value + y->value;
}
|
|
Relationships 
Relationships