Implemented Feedback

benchmarks/c/miscellaneous/nondet_loop.c

@@ -1,6 +1,6 @@
 #include <stdint.h>
 #include <assert.h>
-#include "dat3m.h"
+#include <dat3m.h>
 
 int main()
 {

benchmarks/c/miscellaneous/propagatableSideEffects.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 #include <assert.h>
-#include "dat3m.h"
+#include <dat3m.h>
 
 // This test makes sure that we do not accidentally cut off side-effect-full loops
 // whose side-effects were propagated by constant propagation

benchmarks/c/miscellaneous/thread_loop.c

@@ -1,6 +1,6 @@
 #include <pthread.h>
 #include <stdatomic.h>
-#include "dat3m.h"
+#include <dat3m.h>
 
 /*
     The test shows thread creation inside loops

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -57,8 +57,6 @@
 import static java.lang.Boolean.TRUE;
 import static java.lang.String.valueOf;
 
-;
-
 @Options
 public class Dartagnan extends BaseOptions {
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java

@@ -120,26 +120,15 @@ public Collection<INonDet> getConstants() {
         return Collections.unmodifiableCollection(constants);
     }
 
-    /**
-     * Iterates all events in this program.
-     *
-     * @return {@code globalId}-ordered complete sequence of all events in this program.
-     */
     public List<Event> getThreadEvents() {
+        Preconditions.checkState(!threads.isEmpty(), "The program has no threads yet.");
         List<Event> events = new ArrayList<>();
         for (Function func : threads) {
             events.addAll(func.getEvents());
         }
         return events;
     }
 
-    /**
-     * Iterates a subset of events in this program.
-     *
-     * @param cls Class of events to be selected.
-     * @param <T> Desired subclass of {@link Event}.
-     * @return {@code globalId}-ordered complete sequence of all events of class {@code cls} in this program.
-     */
     public <T extends Event> List<T> getThreadEvents(Class<T> cls) {
         return getThreadEvents().stream().filter(cls::isInstance).map(cls::cast).collect(Collectors.toList());
     }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java

@@ -3,6 +3,7 @@
 import com.dat3m.dartagnan.exception.MalformedProgramException;
 import com.dat3m.dartagnan.expression.type.FunctionType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.EventFactory;
@@ -16,6 +17,7 @@
 import java.math.BigInteger;
 import java.util.List;
 import java.util.stream.IntStream;
+import java.util.stream.Stream;
 
 /*
     This pass collects all Malloc events in the program and for each of them it:
@@ -38,14 +40,12 @@ public void run(Program program) {
     }
 
     private void processMallocs(Program program) {
-        for (Thread thread : program.getThreads()) {
-            for (Malloc malloc : thread.getEvents(Malloc.class)) {
-                final MemoryObject allocatedObject = program.getMemory().allocate(getSize(malloc), false);
-                final Local local = EventFactory.newLocal(malloc.getResultRegister(), allocatedObject);
-                local.addTags(Tag.Std.MALLOC);
-                local.copyAllMetadataFrom(malloc);
-                malloc.replaceBy(local);
-            }
+        for (Malloc malloc : program.getThreadEvents(Malloc.class)) {
+            final MemoryObject allocatedObject = program.getMemory().allocate(getSize(malloc), false);
+            final Local local = EventFactory.newLocal(malloc.getResultRegister(), allocatedObject);
+            local.addTags(Tag.Std.MALLOC);
+            local.copyAllMetadataFrom(malloc);
+            malloc.replaceBy(local);
         }
     }
 
@@ -80,12 +80,12 @@ public void moveAndAlignMemoryObjects(Memory memory) {
     }
 
     private void createInitEvents(Program program) {
-        final List<Thread> threads = program.getThreads();
         final boolean isLitmus = program.getFormat() == Program.SourceLanguage.LITMUS;
         final TypeFactory types = TypeFactory.getInstance();
         final FunctionType initThreadType = types.getFunctionType(types.getVoidType(), List.of());
 
-        int nextThreadId = threads.get(threads.size() - 1).getId() + 1;
+        int nextThreadId = Stream.concat(program.getThreads().stream(), program.getFunctions().stream())
+                .mapToInt(Function::getId).max().getAsInt() + 1;
         for(MemoryObject memObj : program.getMemory().getObjects()) {
             // The last case "heuristically checks" if Smack generated initialization or not:
             // if any field is statically initialized, then likely everything is initialized.