Merge pull request #2447 from lf-lang/verifier-cbmc-uclid-parsing-fix

Fix actions without payloads and fix Uclid parsing error
lf-lang · Dec 9, 2024 · f94394a · f94394a
2 parents 3153e70 + 536c1f6
commit f94394a
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 9 deletions.
diff --git 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
@@ -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();