0001806: Error in coq code generated by wp - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001806

Frama-C

Plug-in > wp

public

2014-06-12 09:53

2019-03-08 15:32

Reporter

davyg

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C Neon-20140301

Target Version

Fixed in Version

Summary

0001806: Error in coq code generated by wp

Description

There is a typing error with some code generated by wp.

For example this script :

_Bool g()
{
    return 0;
}

//@ensures x == (!!\result == !!x);
_Bool f(_Bool x)
{
    return g();
}

When using prover coq from wp generates :

Goal
  forall (f_0 x_0 : Z),
  ((is_uint32 f_0%Z)) ->
  ((is_uint32 x_0%Z)) ->
  ((((Zneq_bool 0 x_0))
    = ((Zeq_bool ((Zneq_bool 0 f_0)) ((Zneq_bool 0 x_0)))))%Z)%Z.

Proof.
(* auto with zarith. *)
Qed.

which produce this coq error on "Zneq_bool 0 f_0":

Error: In environment
f_0 : int
x_0 : int
The term "Zneq_bool 0 f_0" has type "bool" while it is expected to have type
"int".

Steps To Reproduce

Just use the C example with wp/coq as prover (with the gui for example because else wp consider that the script fails and does not print the error)

Tags

No tags attached.

Attached Files

Relationships

Notes
There are no notes attached to this issue.

Issue History
Date Modified	Username	Field	Change
2014-06-12 09:53	davyg	New Issue
2014-06-12 09:53	davyg	Status	new => assigned
2014-06-12 09:53	davyg	Assigned To	=> correnson
2014-06-12 12:53	correnson	Relationship added	duplicate of 0001587
2014-06-12 12:55	correnson	Relationship deleted	0001587