Strange Windows bug --- related to #2130

[grosu]

Trying to figure out what's going on with the non-termination reported by @cos in #2130, I ran into a very strange bug. When kompiling and executing programs by hand, I got the error I reported under #2130 (see it also in the output below) on all programs. When executing with ktest, it hanged. I thought ktest was the problem, but no, the problem appears also when just mentioning the absolute path to your definition in the kompile command line:

D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>ls
NOTES.md  exercises  kool-typed-static.k  tests

D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>kompile kool-typed-static.k
D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>ls
NOTES.md  exercises  kool-typed-static-kompiled  kool-typed-static.k  tests

D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>krun ..\programs\field.kool
(error "line 2 column 30: unknown constant null")
<generatedTop> <T> <tasks> <task> <k> stuck ( class ( Object ) . ( class ( Main ) . Main ) ) ~> #freezer_(_)1 ( .Exps ) ~> discard ~> class ( Main ) ~> #freezer_;0 ( ) </k> <tenv> .Map </tenv> .CtenvTCell <return> void </return> <inClass> Main </inClass> </task> <task> <k> stuck ( class ( Object ) . ( class ( Main ) . a ) ) ~> #freezer_,_1 ( string , .Exps ) ~> #freezer_,_0 ( "a = " ) ~> #freezerprint(_);0 ( ) </k> <tenv> .Map </tenv> .CtenvTCell <return> void </return> <inClass> Main </inClass> </task> </tasks> <classes> <class> <className> Main </className> <extends> Object </extends> <extendsAll> SetItem ( Object ) </extendsAll> <ctenv> Main |-> ( ( void , .Exps ) -> void ) a |-> int </ctenv> </class> </classes> </T> <out> ListItem ( #ostream ( #write ( 1 , "" +String ( "Member \"" +String Id2String ( class ( Main ) . a ) +String "\" not declared! (see class \"" +String "Main" +String "\")\n" ) ) ~> 1 ) ) ListItem ( "on" ) ListItem ( #buffer ( "" ) ) ListItem ( "Member \"" +String Id2String ( class ( Main ) . Main ) +String "\" not declared! (see class \"" +String "Main" +String "\")\n" ) </out> </generatedTop>
[Warning] Critical: failed to translate smtlib expression:
(declare-fun _340 () Bool)
(assert (and (= _340 true) (= null true)))
D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>rm -r kool-typed-static-kompiled

D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>kompile "D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static\kool-typed-static.k"
D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>ls
NOTES.md  exercises  kool-typed-static-kompiled  kool-typed-static.k  tests

D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>krun ..\programs\field.kool
Terminate batch job (Y/N)? Y

D:\github\kframework\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>

So if I kompile with the absolute path to the definition, then it hangs (I stopped the last krun command above after 2 minutes of waiting).

[cos]

My best guess is that the absolute path somehow messes some require. I am not very familiar with that part of the code base -- it is the frontend we're aiming to improve. @andreistefanescu should probably guess which module/require is missing and I'll look into fixing it over the weekend.

The non-termination is likely unrelated. The SMT error likely prevents the execution from reaching the infinite loop.