From fc1b5cfd617db026b42a2a6129a0088172490db5 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 8 Nov 2013 18:45:11 +0100
Subject: [PATCH] Fix problems compiling LetTuple, parametrize instrumented
reads
---
src/main/scala/leon/codegen/CodeGenParams.scala | 6 +++---
src/main/scala/leon/codegen/CodeGeneration.scala | 11 +++++------
2 files changed, 8 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGenParams.scala b/src/main/scala/leon/codegen/CodeGenParams.scala
index b37325747..743b2682d 100644
--- a/src/main/scala/leon/codegen/CodeGenParams.scala
+++ b/src/main/scala/leon/codegen/CodeGenParams.scala
@@ -2,9 +2,9 @@ package leon
package codegen
case class CodeGenParams (
- maxFunctionInvocations: Int = -1,
- checkContracts: Boolean = false
-
+ maxFunctionInvocations: Int = -1, // Monitor calls and abort execution if more than X calls
+ checkContracts: Boolean = false, // Generate calls that checks pre/postconditions
+ doInstrument: Boolean = true // Instrument reads to case classes (mainly for vanuatoo)
) {
val recordInvocations = maxFunctionInvocations > -1
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 2f3429ed0..c3b799b5b 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -137,6 +137,7 @@ object CodeGeneration {
ch << instr
count += 1
}
+ ch << POP
mkExpr(b, ch)(env.withVars(withSlots.toMap))
case IntLiteral(v) =>
@@ -525,8 +526,6 @@ object CodeGeneration {
cf
}
- var doInstrument = true
-
/**
* Instrument read operations
*/
@@ -536,7 +535,7 @@ object CodeGeneration {
ccd.fields.zipWithIndex.find(_._1.id == id) match {
case Some((f, i)) =>
val cName = defToJVMName(ccd)
- if (doInstrument) {
+ if (env.params.doInstrument) {
ch << DUP << DUP
ch << GetField(cName, instrumentedField, "I")
ch << Ldc(1)
@@ -570,7 +569,7 @@ object CodeGeneration {
val namesTypes = ccd.fields.map { vd => (vd.id.name, typeToJVM(vd.tpe)) }
// definition of the constructor
- if(!doInstrument && ccd.fields.isEmpty) {
+ if(!env.params.doInstrument && ccd.fields.isEmpty) {
cf.addDefaultConstructor
} else {
@@ -582,7 +581,7 @@ object CodeGeneration {
).asInstanceOf[U2])
}
- if (doInstrument) {
+ if (env.params.doInstrument) {
val fh = cf.addField("I", instrumentedField)
fh.setFlags(FIELD_ACC_PUBLIC)
}
@@ -592,7 +591,7 @@ object CodeGeneration {
cch << ALoad(0)
cch << InvokeSpecial(pName.getOrElse("java/lang/Object"), constructorName, "()V")
- if (doInstrument) {
+ if (env.params.doInstrument) {
cch << ALoad(0)
cch << Ldc(0)
cch << PutField(cName, instrumentedField, "I")
--
GitLab