diff --git a/core/src/main/java/org/lflang/analyses/uclid/CbmcGenerator.java b/core/src/main/java/org/lflang/analyses/uclid/CbmcGenerator.java index 7daed7bd17..3f2f90d766 100644 --- a/core/src/main/java/org/lflang/analyses/uclid/CbmcGenerator.java +++ b/core/src/main/java/org/lflang/analyses/uclid/CbmcGenerator.java @@ -145,6 +145,7 @@ protected void generateAPIFunctions() { private void generatePortOrActionStructAndNondet( TypedVariable tv, Reactor reactor, String reactionName) { assert tv instanceof Port || tv instanceof Action; // Only ports and actions are allowed. + boolean hasTypedValue = tv.getType() != null; code.pr("typedef struct {"); code.indent(); // NOTE: The following fields are required to be the first ones so that @@ -158,7 +159,7 @@ private void generatePortOrActionStructAndNondet( // "// lf_token_t* token;", // From token_template_t // "// size_t length;", // From token_template_t "bool is_present;", - tv.getType().getId() + " value;"); + hasTypedValue ? tv.getType().getId() + " value;" : ""); code.pr(struct_body); code.unindent(); String name = getTypeName(reactor, tv); @@ -171,9 +172,11 @@ private void generatePortOrActionStructAndNondet( Argument is_present = reactionData.new Argument(); is_present.setTgtType("bool"); reactionData.getType(name).put("is_present", is_present); - Argument value = reactionData.new Argument(); - value.setTgtType(tv.getType().getId()); - reactionData.getType(name).put("value", value); + if (hasTypedValue) { + Argument value = reactionData.new Argument(); + value.setTgtType(tv.getType().getId()); + reactionData.getType(name).put("value", value); + } } /** Instantiate the struct type for an input port. */ diff --git a/core/src/main/java/org/lflang/analyses/uclid/UclidFSMGenerator.java b/core/src/main/java/org/lflang/analyses/uclid/UclidFSMGenerator.java index 1943815d98..97916fd657 100644 --- a/core/src/main/java/org/lflang/analyses/uclid/UclidFSMGenerator.java +++ b/core/src/main/java/org/lflang/analyses/uclid/UclidFSMGenerator.java @@ -306,8 +306,11 @@ private void generateUclidModule() { TypedVariable tv = all.get(j); String type = reactorDef.getName() + "_" + tv.getName() + "_t"; reactionData.types.get(type).get("is_present").setUclType("boolean"); - String uclid_type = getUclidTypeFromCType(tv.getType().getId(), false); - reactionData.types.get(type).get("value").setUclType(uclid_type); + boolean hasTypedValue = tv.getType() != null; + if (hasTypedValue) { + String uclid_type = getUclidTypeFromCType(tv.getType().getId(), false); + reactionData.types.get(type).get("value").setUclType(uclid_type); + } } Boolean hasSelf = reactorDef.getParameters().size() + reactorDef.getStateVars().size() > 0; if (hasSelf) { @@ -395,9 +398,15 @@ private void generateRecordTypes() { code.pr("["); code.indent(); code.pr("(\"is_present\", UBool),"); - String dtype = tv.getType().getId(); - String uclid_type = getUclidTypeFromCType(dtype, true); - code.pr("(\"value\", " + uclid_type + "),"); + boolean hasTypedValue = tv.getType() != null; + if (hasTypedValue) { + String dtype = tv.getType().getId(); + String uclid_type = getUclidTypeFromCType(dtype, true); + code.pr("(\"value\", " + uclid_type + "),"); + } + else { + code.pr("(\"value\", " + "UclidBVType(1)" + "), # Dummy field"); // Print a dummy field here to fix the Uclid parse error. + } code.unindent(); code.pr("]"); code.unindent();