0001603: Errors in coq files generated by WP - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0001603

Frama-C

Plug-in > wp

public

2014-01-16 08:33

2014-03-13 15:57

Reporter

Anne

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Fluorine-20130601

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001603: Errors in coq files generated by WP

Description

I noticed some errors in the coq files generated by WP:
- real_of_int not defined,
- is_float32 : R -> Prop but used as bool (is_float32 f_0%R))%R=true)
- let x_0 := ((Zeq_bool 1 t_0))%Z in ... x_0 used both as bool and as Prop

Additional Information

The example is the foo.c file posted on [Frama-c-discuss] by David Mentre yesterday evening (15/01/2014 - 18:30)

Tags

No tags attached.

Relationships

Notes
(0004423) Anne (reporter) 2014-01-20 09:20	Another error : Goal let a_0 := (shift ((global (G_X_749)%Z)) 0%Z) in ... Error: The term "global G_X_749" has type "addr" while it is expected to have type "nat -> ?1".

(0004493) correnson (manager) 2014-02-05 13:42	Fixed in trunk development version

(0004494) correnson (manager) 2014-02-05 13:43	Fixed during why-3 migration

Issue History
Date Modified	Username	Field	Change
2014-01-16 08:33	Anne	New Issue
2014-01-16 08:33	Anne	Status	new => assigned
2014-01-16 08:33	Anne	Assigned To	=> correnson
2014-01-20 09:20	Anne	Note Added: 0004423
2014-02-05 13:42	correnson	Note Added: 0004493
2014-02-05 13:43	correnson	Note Added: 0004494
2014-02-05 13:43	correnson	Status	assigned => resolved
2014-02-05 13:43	correnson	Resolution	open => fixed
2014-03-13 15:56	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-03-13 15:57	signoles	Status	resolved => closed

Copyright © 2000 - 2018 MantisBT Team