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

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002325Frama-CGraphical User Interfacepublic2017-09-01 10:08
Reportermehdi 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in VersionFrama-C GIT, precise the release id 
Summary0002325: Make it build on bytecode architectures
DescriptionHi,

Frama-C's GUI doesn't build on bytecode only architecture because the Makefile always depend on TARGET_GUI which may contain native objects.

Please find attached a simple patch that fixes this issue.
TagsNo tags attached.
Attached Files
  • patch file icon 0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch (1,232 bytes) 2017-08-11 18:45 -
    From: Mehdi Dogguy <mehdi@debian.org>
    Date: Wed, 21 Dec 2016 14:14:24 +0100
    Subject: gui.byte needs TARGETS_GUI_BYTE only
    
    ---
     share/Makefile.dynamic | 8 ++++++--
     1 file changed, 6 insertions(+), 2 deletions(-)
    
    diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
    index fbdd26a..ac4ee23 100644
    --- a/share/Makefile.dynamic
    +++ b/share/Makefile.dynamic
    @@ -188,14 +188,18 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
     TARGETS := $(TARGET_META) $(TARGET_CMI)
     TARGETS_TOP := $(TARGET_TOP_CMO) $(TARGET_TOP_CMX) \
     	       $(TARGET_TOP_CMA) $(TARGET_TOP_CMXS)
    -TARGETS_GUI := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO) \
    -               $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS)
    +TARGETS_GUI_BYTE := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO)
    +TARGET_GUI := $(TARGETS_GUI_BYTE) $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS)
     TARGETS_BYTE:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMO) $(TARGET_TOP_CMA)
     TARGETS_OPT:=  $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX) $(TARGET_TOP_CMXS)
     
     byte:: $(TARGETS_BYTE)
     opt:: $(TARGETS_OPT)
    +ifeq ($(OCAMLBEST),byte)
    +gui:: $(TARGETS_GUI_BYTE)
    +else
     gui:: $(TARGETS_GUI)
    +endif
     
     # do not define additional targets if you come from the Frama-C Makefile
     ifneq ($(FRAMAC_INTERNAL),yes)
    
    patch file icon 0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch (1,232 bytes) 2017-08-11 18:45 +

-Relationships
+Relationships

-Notes

~0006453

maroneze (administrator)

Thanks for the patch.

There is just a very minor typo (a missing S in TARGET_GUI), but it seems to work fine and we'll try incorporate it into the next release.

~0006456

yakobowski (manager)

Fixed in Phosphorus bugfix (https://github.com/Frama-C/Frama-C-snapshot/commit/30b819710d7630dfaa9f1b434585c62265520d11)
+Notes

-Issue History
Date Modified Username Field Change
2017-08-11 18:45 mehdi New Issue
2017-08-11 18:45 mehdi Status new => assigned
2017-08-11 18:45 mehdi Assigned To => maroneze
2017-08-11 18:45 mehdi File Added: 0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch
2017-08-30 16:47 maroneze Note Added: 0006453
2017-08-30 16:47 maroneze Status assigned => resolved
2017-08-30 16:47 maroneze Fixed in Version => Frama-C 16-Sulfur
2017-08-30 16:47 maroneze Resolution open => fixed
2017-09-01 10:08 yakobowski Note Added: 0006456
2017-09-01 10:08 yakobowski Status resolved => closed
2017-09-01 10:08 yakobowski Fixed in Version Frama-C 16-Sulfur => Frama-C GIT, precise the release id
+Issue History