Making nondet calls have a single null parameter

Author: JohnDumbell

env-model-generator/src/createEntryPoint.ts

@@ -1,7 +1,7 @@
 import * as fs from "fs-extra";
 import { ConfigParseError } from "./configParseError";
 import { Argument, EntryPoint, EntryPointConfig } from "./entryPointConfig";
-import { Cast, Class, Declaration, Expression, FnCall, FnStatement, Method, Statement, StringConstant } from "./javaCode";
+import { Cast, Class, Declaration, Expression, FnCall, FnStatement, Method, Null, Statement, StringConstant } from "./javaCode";
 import { Repository } from "./model";
 import { makeIdentifier } from "./utils";
 
@@ -52,7 +52,7 @@ function createEntryPoint(entryPoint: EntryPoint): Method {
 function getClassConstructionCall(className: string, isContextRequired: boolean): [ Expression, boolean ] {
   const classBeanId = Repository.tryGetIdByClass(className);
   if (classBeanId === undefined) {
-    return [ new FnCall("org.cprover.CProver.nondetWithoutNull", []), isContextRequired ];
+    return [ new FnCall("org.cprover.CProver.nondetWithoutNull", [new Null()]), isContextRequired ];
   } else {
     const classBean = Repository.tryGet(classBeanId);
     if (classBean === undefined)

env-model-generator/src/model.ts

@@ -240,7 +240,7 @@ export class UndefinedBean implements IBean {
       new Method(
         `public ${this.typeName} ${this.getter}()`,
         [
-          new Return(new FnCall("org.cprover.CProver.nondetWithNull", [])),
+          new Return(new FnCall("org.cprover.CProver.nondetWithNull", [new Null()])),
         ],
         []),
         new BlankLine(),