diff --git a/regression/cbmc-java/war-file1/sample.war b/regression/cbmc-java/war-file1/sample.war
new file mode 100644
index 00000000000..0a127e6bd1f
Binary files /dev/null and b/regression/cbmc-java/war-file1/sample.war differ
diff --git a/regression/cbmc-java/war-file1/test.desc b/regression/cbmc-java/war-file1/test.desc
new file mode 100644
index 00000000000..3f64bfbb2bd
--- /dev/null
+++ b/regression/cbmc-java/war-file1/test.desc
@@ -0,0 +1,9 @@
+CORE
+sample.war
+--function mypackage.Hello.doGet --cover location
+^EXIT=0$
+^SIGNAL=0$
+\*\* 25 of 26 covered
+--
+--
+war file source https://tomcat.apache.org/tomcat-6.0-doc/appdev/sample/
diff --git a/regression/cbmc-java/war-file1/url.txt b/regression/cbmc-java/war-file1/url.txt
new file mode 100644
index 00000000000..d5ce0da75a7
--- /dev/null
+++ b/regression/cbmc-java/war-file1/url.txt
@@ -0,0 +1 @@
+https://tomcat.apache.org/tomcat-6.0-doc/appdev/sample/
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 0a6e3c4dd58..a08c622276c 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -632,7 +632,8 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   if((has_suffix(file_name, ".class") ||
-      has_suffix(file_name, ".jar")) &&
+      has_suffix(file_name, ".jar") ||
+      has_suffix(file_name, ".war")) &&
      final())
     return true;
 
diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp
index bc065d7a0e9..ab04aa46d14 100644
--- a/src/java_bytecode/jar_file.cpp
+++ b/src/java_bytecode/jar_file.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <json/json_parser.h>
 #include <util/suffix.h>
+#include <util/suffix.h>
 #include <util/invariant.h>
 
 void jar_filet::open(
@@ -53,6 +54,12 @@ void jar_filet::open(
 #endif
       INVARIANT(file_name.size()==filename_len-1, "no \\0 found in file name");
 
+      // remove WAR class prefix
+      // cf. https://en.wikipedia.org/wiki/WAR_(file_format)
+      const std::string war_class_prefix("WEB-INF/classes/");
+      if(has_prefix(file_name, war_class_prefix))
+        file_name=file_name.substr(war_class_prefix.length());
+
       // non-class files are loaded in any case
       bool add_file=!has_suffix(file_name, ".class");
       // load .class file only if they match regex / are in match set
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index bac7157df5c..bb7bb1f170a 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -68,27 +68,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     java_cp_include_files=cmd.get_value("java-cp-include-files");
     // load file list from JSON file
     if(java_cp_include_files[0]=='@')
-    {
-      jsont json_cp_config;
-      if(parse_json(
-           java_cp_include_files.substr(1),
-           get_message_handler(),
-           json_cp_config))
-        throw "cannot read JSON input configuration for JAR loading";
-
-      if(!json_cp_config.is_object())
-        throw "the JSON file has a wrong format";
-      jsont include_files=json_cp_config["jar"];
-      if(!include_files.is_array())
-         throw "the JSON file has a wrong format";
-
-      // add jars from JSON config file to classpath
-      for(const jsont &file_entry : include_files.array)
-      {
-        assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar"));
-        config.java.classpath.push_back(file_entry.value);
-      }
-    }
+      load_from_archive_files(java_cp_include_files.substr(1));
   }
   else
     java_cp_include_files=".*";
@@ -98,7 +78,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 
 std::set<std::string> java_bytecode_languaget::extensions() const
 {
-  return { "class", "jar" };
+  return { "class", "jar", "war" };
 }
 
 void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
@@ -130,7 +110,7 @@ bool java_bytecode_languaget::parse(
     // override main_class
     main_class=java_class_loadert::file_to_class_name(path);
   }
-  else if(has_suffix(path, ".jar"))
+  else if(has_suffix(path, ".jar") || has_suffix(path, ".war"))
   {
     // build an object to potentially limit which classes are loaded
     java_class_loader_limitt class_loader_limit(
@@ -462,3 +442,45 @@ bool java_bytecode_languaget::to_expr(
 java_bytecode_languaget::~java_bytecode_languaget()
 {
 }
+
+void java_bytecode_languaget::load_from_archive_files(
+  const std::string &json_config)
+{
+  jsont json_cp_config;
+  if(parse_json(
+       json_config,
+       get_message_handler(),
+       json_cp_config))
+    throw "cannot read JSON input configuration for JAR/WAR loading";
+
+  if(!json_cp_config.is_object())
+    throw "the JSON file has a wrong format";
+  jsont include_jar_files=json_cp_config["jar"];
+  if(!include_jar_files.is_null())
+  {
+    if(!include_jar_files.is_array())
+      throw "the JSON file has a wrong format";
+
+    // add jars from JSON config file to classpath
+    for(const jsont &file_entry : include_jar_files.array)
+    {
+      assert(file_entry.is_string() &&
+             has_suffix(file_entry.value, ".jar"));
+      config.java.classpath.push_back(file_entry.value);
+    }
+  }
+  jsont include_war_files=json_cp_config["war"];
+  if(!include_war_files.is_null())
+  {
+    if(!include_war_files.is_array())
+      throw "the JSON file has a wrong format";
+
+    // add wars from JSON config file to classpath
+    for(const jsont &file_entry : include_war_files.array)
+    {
+      assert(file_entry.is_string() &&
+             has_suffix(file_entry.value, ".war"));
+      config.java.classpath.push_back(file_entry.value);
+    }
+  }
+}
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index a688440e64d..afa94f03792 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -139,6 +139,7 @@ class java_bytecode_languaget:public languaget
 protected:
   bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &);
   const select_pointer_typet &get_pointer_type_selector() const;
+  void load_from_archive_files(const std::string &);
 
   irep_idt main_class;
   std::vector<irep_idt> main_jar_classes;
diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp
index 675e137227c..c154b51b009 100644
--- a/src/java_bytecode/java_class_loader.cpp
+++ b/src/java_bytecode/java_class_loader.cpp
@@ -109,7 +109,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree(
   for(const auto &cp : config.java.classpath)
   {
     // in a JAR?
-    if(has_suffix(cp, ".jar"))
+    if(has_suffix(cp, ".jar") || has_suffix(cp, ".war"))
     {
       read_jar_file(class_loader_limit, cp);
 
@@ -119,7 +119,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree(
 
       if(jm_it!=jm.entries.end())
       {
-        debug() << "Getting class `" << class_name << "' from JAR "
+        debug() << "Getting class `" << class_name << "' from {J,W}AR "
                 << cp << eom;
 
         std::string data=jar_pool(class_loader_limit, cp)