From daccc2928e6410c4e8c886ea7d019fd9a071b931 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 29 Mar 2015 19:57:16 +0200
Subject: Omission: forgot to treat pointer values in bool_of_val and
 sem_notbool.

---
 cfrontend/SimplExpr.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'cfrontend/SimplExpr.v')

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 36fe07ae..097dc589 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -18,6 +18,7 @@ Require Import Errors.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
+Require Import Memory.
 Require Import AST.
 Require Import Ctypes.
 Require Import Cop.
@@ -129,7 +130,7 @@ Function eval_simpl_expr (a: expr) : option val :=
 Function makeif (a: expr) (s1 s2: statement) : statement :=
   match eval_simpl_expr a with
   | Some v =>
-      match bool_val v (typeof a) with
+      match bool_val v (typeof a) Mem.empty with
       | Some b => if b then s1 else s2
       | None   => Sifthenelse a s1 s2
       end
-- 
cgit