---
layout: fc_discuss_archives
title: Message 3 from Frama-C-discuss on October 2015
---
[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: kurt at roeckx.be (Kurt Roeckx)
- Date: Sat, 3 Oct 2015 21:02:50 +0200
- In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB172@Mail1.FCMD.local>
- References: <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> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB172@Mail1.FCMD.local>
On Sat, Oct 03, 2015 at 02:32:07PM -0400, Dharmalingam Ganesan wrote:
> /*@ assert x*x < 0 ;*/
Please note that the evaluation does not happen in a fixed size
integer. Since x is positive, x*x will always be positive in that
evaluation.
Kurt