Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:42 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002378Frama-Cptestspublic2020-02-17 18:08
Reportermadroach 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Platformbytecode-onlyOSOpenBSDOS Version6.3
Product Version 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002378: Bytecode only compilation fails when linking to stdlib
DescriptionCompiling bytecode only fails with this error:

ocamlfind ocamlc -I ptests -dtypes -vmthread -g -o bin/ptests.byte unix.cma threads.cma str.cma dynlink.cma ptests/ptests_config.ml ptests/ptests.ml
File "ptests/ptests.ml", line 1:
Error: Required module `Uchar' is unavailable
Steps To ReproduceCompile OCaml >=4.03 without optimizing compilers.
Use this compiler to build frama-c
TagsNo tags attached.
Attached Files
  • ? file icon patch-configure_in (1,400 bytes) 2019-02-24 23:55 -
    $OpenBSD$
    
    Use system threads if available - even on bytecode builds.
    Vmthreads are broken and deprecated.
    
    Index: configure.in
    --- configure.in.orig
    +++ configure.in
    @@ -436,23 +436,23 @@ else
         EXE=
       fi
     
    -  if test "$OCAMLBEST" = opt; then
    -    # OCaml native threads
    -    AC_MSG_CHECKING([OCaml native threads])
    -    echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
    -    if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
    -         test_native_threads.ml) 2> /dev/null ;
    -    then
    -      HAS_NATIVE_THREADS=yes
    -      AC_MSG_RESULT([ok.]);
    -    else
    -      HAS_NATIVE_THREADS=no
    -      AC_MSG_WARN([unsupported.]);
    -    fi
    -    rm -f test_native_threads*;
    +  # OCaml native threads
    +  AC_MSG_CHECKING([OCaml native threads])
    +  echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
    +  if
    +    test "$OCAMLBEST" = opt &&
    +    ($OCAMLOPT -thread -o test_native_threads unix.cma threads.cma \
    +       test_native_threads.ml) 2> /dev/null ||
    +    ($OCAMLC -thread -o test_native_threads unix.cma threads.cma \
    +       test_native_threads.ml) 2> /dev/null
    +  then
    +    HAS_NATIVE_THREADS=yes
    +    AC_MSG_RESULT([ok.]);
       else
    -    HAS_NATIVE_THREADS=no; # no native compilation anyway
    +    HAS_NATIVE_THREADS=no
    +    AC_MSG_WARN([unsupported.]);
       fi
    +  rm -f test_native_threads*;
     fi
     
     # C and POSIX standard headers used by C bindings.
    
    ? file icon patch-configure_in (1,400 bytes) 2019-02-24 23:55 +
  • ? file icon patch-Makefile (888 bytes) 2019-02-25 02:01 -
    $OpenBSD$
    
    don't try to install cmx* files on bytecode builds.
    
    Index: Makefile
    --- Makefile.orig
    +++ Makefile
    @@ -1863,14 +1863,16 @@ install:: install-lib
     	if [ -d "$(FRAMAC_PLUGIN)" ]; then \
     	  $(CP)  $(PLUGIN_DYN_CMI_LIST) $(PLUGIN_META_LIST) \
     		 $(FRAMAC_PLUGINDIR); \
    -	  $(CP)  $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
    +	  $(CP)  $(PLUGIN_DYN_CMO_LIST) \
    +		 $(if $(filter opt, $(OCAMLBEST)), $(PLUGIN_DYN_CMX_LIST),) \
     		 $(FRAMAC_PLUGINDIR)/top; \
     	fi
     	$(PRINT_INSTALL) gui plug-ins
     	if [ -d "$(FRAMAC_PLUGIN_GUI)" -a "$(PLUGIN_DYN_GUI_EXISTS)" = "yes" ]; \
     	then \
     	  $(CP) $(patsubst %.cma,%.cmi,$(PLUGIN_DYN_GUI_CMO_LIST:.cmo=.cmi)) \
    -		$(PLUGIN_DYN_GUI_CMO_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \
    +		$(PLUGIN_DYN_GUI_CMO_LIST) \
    +		$(if $(filter opt, $(OCAMLBEST)), $(PLUGIN_DYN_GUI_CMX_LIST),) \
     		$(FRAMAC_PLUGINDIR)/gui; \
     	fi
     	$(PRINT_INSTALL) man pages
    
    ? file icon patch-Makefile (888 bytes) 2019-02-25 02:01 +
  • ? file icon patch-configure_in_2 (1,282 bytes) 2019-08-29 00:36 -
    $OpenBSD: patch-configure_in,v 1.1 2019/03/04 12:51:12 chrisz Exp $
    
    Use system threads if available - even on bytecode builds.
    Vmthreads are broken and deprecated.
    
    Index: configure.in
    --- configure.in.orig
    +++ configure.in
    @@ -446,23 +446,19 @@ else
         EXE=
       fi
     
    -  if test "$OCAMLBEST" = opt; then
    -    # OCaml native threads
    -    AC_MSG_CHECKING([OCaml native threads])
    -    echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
    -    if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
    -         test_native_threads.ml) 2> /dev/null ;
    -    then
    -      HAS_NATIVE_THREADS=yes
    -      AC_MSG_RESULT([ok.]);
    -    else
    -      HAS_NATIVE_THREADS=no
    -      AC_MSG_WARN([unsupported.]);
    -    fi
    -    rm -f test_native_threads*;
    +  AC_MSG_CHECKING([OCaml native threads])
    +  echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
    +  if
    +    ($OCAMLC -thread -o test_native_threads unix.cma threads.cma \
    +       test_native_threads.ml) 2> /dev/null
    +  then
    +    HAS_NATIVE_THREADS=yes
    +    AC_MSG_RESULT([ok.]);
       else
    -    HAS_NATIVE_THREADS=no; # no native compilation anyway
    +    HAS_NATIVE_THREADS=no
    +    AC_MSG_WARN([unsupported.]);
       fi
    +  rm -f test_native_threads*;
     fi
     
     # C and POSIX standard headers used by C bindings.
    
    ? file icon patch-configure_in_2 (1,282 bytes) 2019-08-29 00:36 +
  • ? file icon patch-Makefile_2 (2,039 bytes) 2019-08-29 00:46 -
    $OpenBSD: patch-Makefile,v 1.1 2019/03/04 12:51:12 chrisz Exp $
    
    don't try to install cmx* files on bytecode builds.
    
    Index: Makefile
    --- Makefile.orig
    +++ Makefile
    @@ -1234,12 +1234,15 @@ bin/toplevel.opt$(EXE): $(ALL_BATCH_CMX) $(GEN_OPT_LIB
     LIB_KERNEL_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo, $(CMO))
     LIB_KERNEL_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx, $(CMX))
     
    -lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) $(LIB_KERNEL_CMX) lib/fc/META.frama-c
    -	$(PRINT_LINKING) $@ and lib/fc/frama-c.cmxa
    +lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) lib/fc/META.frama-c
    +	$(PRINT_LINKING) $@
     	$(MKDIR) $(FRAMAC_LIB)
    -	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO) $(LIB_KERNEL_CMX)
    +	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO)
     
     lib/fc/frama-c.cmxa: lib/fc/frama-c.cma
    +	$(MKDIR) $(FRAMAC_LIB)
    +	$(PRINT_LINKING) $@
    +	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMX)
     
     ####################
     # (Ocaml) Toplevel #
    @@ -1863,12 +1866,16 @@ clean-install:
     	$(PRINT_RM) "Installation directory"
     	$(RM) -r $(FRAMAC_LIBDIR)
     
    -install-lib: clean-install
    +install-lib-byte: clean-install
     	$(PRINT_INSTALL) kernel API
     	$(MKDIR) $(FRAMAC_LIBDIR)
    -	$(CP) $(LIB_BYTE_TO_INSTALL) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
    -	$(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma frama-c.a frama-c.cmxa META.frama-c)  $(FRAMAC_LIBDIR)
    +	$(CP) $(LIB_BYTE_TO_INSTALL) $(FRAMAC_LIBDIR)
    +	$(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma META.frama-c)  $(FRAMAC_LIBDIR)
     
    +install-lib-opt: install-lib-byte
    +	$(CP) $(LIB_OPT_TO_INSTALL)
    +	$(CP) $(addprefix frama-c.a frama-c.cmxa)
    +
     install-doc-code:
     	$(PRINT_INSTALL) API documentation
     	$(MKDIR) $(FRAMAC_DATADIR)/doc/code
    @@ -1879,7 +1886,7 @@ install-doc-code:
     		| (cd $(FRAMAC_DATADIR)/doc ; tar xf -))
     
     .PHONY: install
    -install:: install-lib
    +install:: install-lib-$(OCAMLBEST)
     	$(PRINT_MAKING) destination directories
     	$(MKDIR) $(BINDIR)
     	$(MKDIR) $(MANDIR)/man1
    
    ? file icon patch-Makefile_2 (2,039 bytes) 2019-08-29 00:46 +
  • ? file icon patch-Makefile_3 (2,091 bytes) 2019-08-30 00:49 -
    $OpenBSD: patch-Makefile,v 1.1 2019/03/04 12:51:12 chrisz Exp $
    
    don't try to build or install cmx* files on bytecode builds.
    
    Index: Makefile
    --- Makefile.orig
    +++ Makefile
    @@ -1234,12 +1234,15 @@ bin/toplevel.opt$(EXE): $(ALL_BATCH_CMX) $(GEN_OPT_LIB
     LIB_KERNEL_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo, $(CMO))
     LIB_KERNEL_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx, $(CMX))
     
    -lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) $(LIB_KERNEL_CMX) lib/fc/META.frama-c
    -	$(PRINT_LINKING) $@ and lib/fc/frama-c.cmxa
    +lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) lib/fc/META.frama-c
    +	$(PRINT_LINKING) $@
     	$(MKDIR) $(FRAMAC_LIB)
    -	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO) $(LIB_KERNEL_CMX)
    +	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO)
     
     lib/fc/frama-c.cmxa: lib/fc/frama-c.cma
    +	$(MKDIR) $(FRAMAC_LIB)
    +	$(PRINT_LINKING) $@
    +	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMX)
     
     ####################
     # (Ocaml) Toplevel #
    @@ -1863,12 +1866,16 @@ clean-install:
     	$(PRINT_RM) "Installation directory"
     	$(RM) -r $(FRAMAC_LIBDIR)
     
    -install-lib: clean-install
    +install-lib-byte: clean-install
     	$(PRINT_INSTALL) kernel API
     	$(MKDIR) $(FRAMAC_LIBDIR)
    -	$(CP) $(LIB_BYTE_TO_INSTALL) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
    -	$(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma frama-c.a frama-c.cmxa META.frama-c)  $(FRAMAC_LIBDIR)
    +	$(CP) $(LIB_BYTE_TO_INSTALL) $(FRAMAC_LIBDIR)
    +	$(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma META.frama-c)  $(FRAMAC_LIBDIR)
     
    +install-lib-opt: install-lib-byte
    +	$(CP) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
    +	$(CP) $(addprefix lib/fc/,frama-c.a frama-c.cmxa)  $(FRAMAC_LIBDIR)
    +
     install-doc-code:
     	$(PRINT_INSTALL) API documentation
     	$(MKDIR) $(FRAMAC_DATADIR)/doc/code
    @@ -1879,7 +1886,7 @@ install-doc-code:
     		| (cd $(FRAMAC_DATADIR)/doc ; tar xf -))
     
     .PHONY: install
    -install:: install-lib
    +install:: install-lib-$(OCAMLBEST)
     	$(PRINT_MAKING) destination directories
     	$(MKDIR) $(BINDIR)
     	$(MKDIR) $(MANDIR)/man1
    
    ? file icon patch-Makefile_3 (2,091 bytes) 2019-08-30 00:49 +

-Relationships
+Relationships

-Notes

~0006752

madroach (reporter)

Last edited: 2019-02-24 23:59

View 2 revisions

I suspect the build error is caused by +vmthreads/stdlib.cma having a different ordering and set of modules than +stdlib.cma.
Since vmthreads are being deprecated anyway I would consider always building with system threads.
Alternatively, do at least prefer system threads even on bytecode builds as is done by the patch I just uploaded.

~0006856

madroach (reporter)

Please commit at least the configure patch.
There is a misunderstanding of what "native system threads" implies in the OCaml world.
Native system threads are available for native and for bytecode compilation and are the only available threading since vmthreads, which were only supported for bytecode, have been dropped.

~0006857

maroneze (administrator)

I hadn't seen this issue before, so in March I applied a similar patch to the Makefile, which should have the same effect as yours, I think (and it should already be available in the latest Frama-C release, 19.0). But the configure patch has not been applied.

We don't currently have an OpenBSD VM to test it, but I tried applying the patch using my fork of Frama-C's Github repository (https://github.com/maroneze/Frama-C-snapshot). If it looks good to you, we'll probably commit it soon.

~0006858

madroach (reporter)

Looks good to me. You might consider applying patch-configure_in_2 instead because it is simpler while yielding the same results. There is no difference in threading between byte- and nativecode anymore.

~0006860

madroach (reporter)

Now also updated to patch-Makefile_2 adding a fix to allow bytecode only installation.

~0006862

maroneze (administrator)

Thanks a lot. I adapted a bit the patch Makefile_2 to make it work, and we will try to integrate it quickly. Concerning the threads detection, though, maybe it's better to completely remove the test from the configure, assuming native threads are always available.

Is there a deadline concerning OpenBSD package releases? In other words, would it be useful if the patches were integrated ASAP, or could it wait for the next Frama-C release (likely sometime in November/December)?

~0006863

madroach (reporter)

Last edited: 2019-08-29 09:55

View 2 revisions

I have no idea which platforms would run Frama-C without threads and therefore no idea whether they need thread-detection.


No need to hurry the release; we are patching Frama-C in our ports.
But it would be nice if we could stop maintaining the patches with the next Frama-C update.

~0006864

virgile (developer)

The fact that vmthreads are deprecated in 4.08 (https://github.com/ocaml/ocaml/pull/2038), with the suggestion to move to system threads regardless of the OS on which the application is run is in my opinion a good hint that assuming native thread support everywhere is not too far fetched.

~0006865

madroach (reporter)

According to https://ocaml.org/learn/portability.html threads are supported everywhere.

~0006867

madroach (reporter)

I'm afraid I forgot to test native code builds, which are broken by my Makefile patch. That's why I just uploaded a fixed 3rd version of the Makefile patch.

~0006869

virgile (developer)

Changes have been merged internally and will be part of Frama-C 20.0 Calcium

~0006953

signoles (manager)

Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2018-06-18 16:48 madroach New Issue
2018-06-18 16:48 madroach Status new => assigned
2018-06-18 16:48 madroach Assigned To => virgile
2018-11-30 10:41 signoles Assigned To virgile => bobot
2019-02-24 23:56 madroach File Added: patch-configure_in
2019-02-24 23:58 madroach Note Added: 0006752
2019-02-24 23:59 madroach Note Edited: 0006752 View Revisions
2019-02-25 02:01 madroach File Added: patch-Makefile
2019-08-27 22:06 madroach Note Added: 0006856
2019-08-28 17:37 maroneze Assigned To bobot => maroneze
2019-08-28 18:04 maroneze Note Added: 0006857
2019-08-29 00:36 madroach File Added: patch-configure_in_2
2019-08-29 00:38 madroach Note Added: 0006858
2019-08-29 00:46 madroach File Added: patch-Makefile_2
2019-08-29 00:47 madroach Note Added: 0006860
2019-08-29 09:14 maroneze Note Added: 0006862
2019-08-29 09:54 madroach Note Added: 0006863
2019-08-29 09:55 madroach Note Edited: 0006863 View Revisions
2019-08-29 10:38 virgile Note Added: 0006864
2019-08-29 12:52 madroach Note Added: 0006865
2019-08-30 00:49 madroach File Added: patch-Makefile_3
2019-08-30 00:50 madroach Note Added: 0006867
2019-09-12 17:44 virgile Note Added: 0006869
2019-09-12 17:44 virgile Status assigned => resolved
2019-09-12 17:44 virgile Fixed in Version => Frama-C 20-Calcium
2019-09-12 17:44 virgile Resolution open => fixed
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006953
+Issue History