0000926: wp-plugin does not generate coq *.v goals.

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

Notes
(0002147) jessie_user (reporter) 2011-08-15 17:54	I have tried it this on 2 different installations of frama-c (carbon-201102)

(0002364) correnson (manager) 2011-09-30 13:31	Use -wp-check coq

(0002365) correnson (manager) 2011-09-30 13:32	Better handling of proof-obilgation exports in future release. Work-around: -wp-check coq

Issue History
Date Modified	Username	Field	Change
2011-08-15 17:53	jessie_user	New Issue
2011-08-15 17:53	jessie_user	Status	new => assigned
2011-08-15 17:53	jessie_user	Assigned To	=> correnson
2011-08-15 17:53	jessie_user	File Added: test_wp_longlong.c
2011-08-15 17:54	jessie_user	Note Added: 0002147
2011-09-30 13:31	correnson	Note Added: 0002364
2011-09-30 13:32	correnson	Note Added: 0002365
2011-09-30 13:32	correnson	Status	assigned => closed
2011-09-30 13:32	correnson	Resolution	open => fixed
2011-09-30 13:35	correnson	Status	closed => resolved
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed